H-Termination proof of /home/matraf/haskell/eval_FullyBlown

MAYBE 3.783 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could not be shown:

↳ HASKELL

  ↳ BR

mainModule Main

((enumFromThen :: () -> () -> [()]) :: () -> () -> [()])

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule Main

((enumFromThen :: () -> () -> [()]) :: () -> () -> [()])

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

The following Function with conditions

toEnum 0 = ()

is transformed to

toEnum vz = toEnum1 vz

toEnum0 True vz = ()

toEnum1 vz = toEnum0 (vz == 0) vz

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

mainModule Main

((enumFromThen :: () -> () -> [()]) :: () -> () -> [()])

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

mainModule Main

(enumFromThen :: () -> () -> [()])

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="enumFromThen",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="enumFromThen wu3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="enumFromThen wu3 wu4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="map toEnum (enumFromThen (fromEnum wu3) (fromEnum wu4))",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="map toEnum (numericEnumFromThen (fromEnum wu3) (fromEnum wu4))",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="map toEnum (iterate (fromEnum wu4 - fromEnum wu3 +) (fromEnum wu3))",fontsize=16,color="black",shape="box"];7 -> 8[label="",style="solid", color="black", weight=3];
8[label="map toEnum (fromEnum wu3 : iterate (fromEnum wu4 - fromEnum wu3 +) (fromEnum wu4 - fromEnum wu3 + fromEnum wu3))",fontsize=16,color="black",shape="box"];8 -> 9[label="",style="solid", color="black", weight=3];
9[label="toEnum (fromEnum wu3) : map toEnum (iterate (fromEnum wu4 - fromEnum wu3 +) (fromEnum wu4 - fromEnum wu3 + fromEnum wu3))",fontsize=16,color="green",shape="box"];9 -> 10[label="",style="dashed", color="green", weight=3];
9 -> 11[label="",style="dashed", color="green", weight=3];
10[label="toEnum (fromEnum wu3)",fontsize=16,color="black",shape="box"];10 -> 12[label="",style="solid", color="black", weight=3];
11 -> 74[label="",style="dashed", color="red", weight=0];
11[label="map toEnum (iterate (fromEnum wu4 - fromEnum wu3 +) (fromEnum wu4 - fromEnum wu3 + fromEnum wu3))",fontsize=16,color="magenta"];11 -> 75[label="",style="dashed", color="magenta", weight=3];
11 -> 76[label="",style="dashed", color="magenta", weight=3];
11 -> 77[label="",style="dashed", color="magenta", weight=3];
12 -> 119[label="",style="dashed", color="red", weight=0];
12[label="toEnum1 (fromEnum wu3)",fontsize=16,color="magenta"];12 -> 120[label="",style="dashed", color="magenta", weight=3];
75[label="wu3",fontsize=16,color="green",shape="box"];76[label="wu4",fontsize=16,color="green",shape="box"];77[label="fromEnum wu3",fontsize=16,color="burlywood",shape="triangle"];380[label="wu3/()",fontsize=10,color="white",style="solid",shape="box"];77 -> 380[label="",style="solid", color="burlywood", weight=9];
380 -> 93[label="",style="solid", color="burlywood", weight=3];
74[label="map toEnum (iterate (fromEnum wu6 - fromEnum wu7 +) (fromEnum wu6 - fromEnum wu7 + wu8))\n  Enum a  Enum b  Enum c",fontsize=16,color="black",shape="triangle"];74 -> 94[label="",style="solid", color="black", weight=3];
120 -> 77[label="",style="dashed", color="red", weight=0];
120[label="fromEnum wu3",fontsize=16,color="magenta"];119[label="toEnum1 wu9",fontsize=16,color="black",shape="triangle"];119 -> 122[label="",style="solid", color="black", weight=3];
93[label="fromEnum ()",fontsize=16,color="black",shape="box"];93 -> 95[label="",style="solid", color="black", weight=3];
94[label="map toEnum (fromEnum wu6 - fromEnum wu7 + wu8 : iterate (fromEnum wu6 - fromEnum wu7 +) (fromEnum wu6 - fromEnum wu7 + (fromEnum wu6 - fromEnum wu7 + wu8)))\n  Enum a  Enum b  Enum c",fontsize=16,color="black",shape="box"];94 -> 96[label="",style="solid", color="black", weight=3];
122[label="toEnum0 (wu9 == Pos Zero) wu9",fontsize=16,color="black",shape="box"];122 -> 124[label="",style="solid", color="black", weight=3];
95[label="Pos Zero",fontsize=16,color="green",shape="box"];96[label="toEnum (fromEnum wu6 - fromEnum wu7 + wu8) : map toEnum (iterate (fromEnum wu6 - fromEnum wu7 +) (fromEnum wu6 - fromEnum wu7 + (fromEnum wu6 - fromEnum wu7 + wu8)))\n  Enum a  Enum b  Enum c",fontsize=16,color="green",shape="box"];96 -> 97[label="",style="dashed", color="green", weight=3];
96 -> 98[label="",style="dashed", color="green", weight=3];
124[label="toEnum0 (primEqInt wu9 (Pos Zero)) wu9",fontsize=16,color="burlywood",shape="box"];382[label="wu9/Pos wu90",fontsize=10,color="white",style="solid",shape="box"];124 -> 382[label="",style="solid", color="burlywood", weight=9];
382 -> 129[label="",style="solid", color="burlywood", weight=3];
383[label="wu9/Neg wu90",fontsize=10,color="white",style="solid",shape="box"];124 -> 383[label="",style="solid", color="burlywood", weight=9];
383 -> 130[label="",style="solid", color="burlywood", weight=3];
97[label="toEnum (fromEnum wu6 - fromEnum wu7 + wu8)\n  Enum a  Enum b  Enum c",fontsize=16,color="blue",shape="box"];384[label="toEnum :: Int -> Char",fontsize=10,color="white",style="solid",shape="box"];97 -> 384[label="",style="solid", color="blue", weight=9];
384 -> 99[label="",style="solid", color="blue", weight=3];
385[label="toEnum :: Int -> Bool",fontsize=10,color="white",style="solid",shape="box"];97 -> 385[label="",style="solid", color="blue", weight=9];
385 -> 100[label="",style="solid", color="blue", weight=3];
386[label="toEnum :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];97 -> 386[label="",style="solid", color="blue", weight=9];
386 -> 101[label="",style="solid", color="blue", weight=3];
387[label="toEnum :: Int -> Ordering",fontsize=10,color="white",style="solid",shape="box"];97 -> 387[label="",style="solid", color="blue", weight=9];
387 -> 102[label="",style="solid", color="blue", weight=3];
388[label="toEnum :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];97 -> 388[label="",style="solid", color="blue", weight=9];
388 -> 103[label="",style="solid", color="blue", weight=3];
389[label="toEnum :: Int -> ()",fontsize=10,color="white",style="solid",shape="box"];97 -> 389[label="",style="solid", color="blue", weight=9];
389 -> 104[label="",style="solid", color="blue", weight=3];
390[label="toEnum :: Int -> Float",fontsize=10,color="white",style="solid",shape="box"];97 -> 390[label="",style="solid", color="blue", weight=9];
390 -> 105[label="",style="solid", color="blue", weight=3];
391[label="toEnum :: Int -> Double",fontsize=10,color="white",style="solid",shape="box"];97 -> 391[label="",style="solid", color="blue", weight=9];
391 -> 106[label="",style="solid", color="blue", weight=3];
392[label="toEnum :: Int -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];97 -> 392[label="",style="solid", color="blue", weight=9];
392 -> 107[label="",style="solid", color="blue", weight=3];
98 -> 74[label="",style="dashed", color="red", weight=0];
98[label="map toEnum (iterate (fromEnum wu6 - fromEnum wu7 +) (fromEnum wu6 - fromEnum wu7 + (fromEnum wu6 - fromEnum wu7 + wu8)))\n  Enum a  Enum b  Enum c",fontsize=16,color="magenta"];98 -> 108[label="",style="dashed", color="magenta", weight=3];
129[label="toEnum0 (primEqInt (Pos wu90) (Pos Zero)) (Pos wu90)",fontsize=16,color="burlywood",shape="box"];394[label="wu90/Succ wu900",fontsize=10,color="white",style="solid",shape="box"];129 -> 394[label="",style="solid", color="burlywood", weight=9];
394 -> 142[label="",style="solid", color="burlywood", weight=3];
395[label="wu90/Zero",fontsize=10,color="white",style="solid",shape="box"];129 -> 395[label="",style="solid", color="burlywood", weight=9];
395 -> 143[label="",style="solid", color="burlywood", weight=3];
130[label="toEnum0 (primEqInt (Neg wu90) (Pos Zero)) (Neg wu90)",fontsize=16,color="burlywood",shape="box"];396[label="wu90/Succ wu900",fontsize=10,color="white",style="solid",shape="box"];130 -> 396[label="",style="solid", color="burlywood", weight=9];
396 -> 144[label="",style="solid", color="burlywood", weight=3];
397[label="wu90/Zero",fontsize=10,color="white",style="solid",shape="box"];130 -> 397[label="",style="solid", color="burlywood", weight=9];
397 -> 145[label="",style="solid", color="burlywood", weight=3];
99[label="toEnum (fromEnum wu6 - fromEnum wu7 + wu8)\n  Enum a  Enum b",fontsize=16,color="black",shape="box"];99 -> 109[label="",style="solid", color="black", weight=3];
100[label="toEnum (fromEnum wu6 - fromEnum wu7 + wu8)\n  Enum a  Enum b",fontsize=16,color="black",shape="box"];100 -> 110[label="",style="solid", color="black", weight=3];
101[label="toEnum (fromEnum wu6 - fromEnum wu7 + wu8)\n  Enum a  Enum b",fontsize=16,color="black",shape="box"];101 -> 111[label="",style="solid", color="black", weight=3];
102[label="toEnum (fromEnum wu6 - fromEnum wu7 + wu8)\n  Enum a  Enum b",fontsize=16,color="black",shape="box"];102 -> 112[label="",style="solid", color="black", weight=3];
103[label="toEnum (fromEnum wu6 - fromEnum wu7 + wu8)\n  Enum a  Enum b",fontsize=16,color="black",shape="box"];103 -> 113[label="",style="solid", color="black", weight=3];
104[label="toEnum (fromEnum wu6 - fromEnum wu7 + wu8)\n  Enum a  Enum b",fontsize=16,color="black",shape="box"];104 -> 114[label="",style="solid", color="black", weight=3];
105[label="toEnum (fromEnum wu6 - fromEnum wu7 + wu8)\n  Enum a  Enum b",fontsize=16,color="black",shape="box"];105 -> 115[label="",style="solid", color="black", weight=3];
106[label="toEnum (fromEnum wu6 - fromEnum wu7 + wu8)\n  Enum a  Enum b",fontsize=16,color="black",shape="box"];106 -> 116[label="",style="solid", color="black", weight=3];
107[label="toEnum (fromEnum wu6 - fromEnum wu7 + wu8)\n  Enum a  Integral b  Enum c",fontsize=16,color="black",shape="box"];107 -> 117[label="",style="solid", color="black", weight=3];
108[label="fromEnum wu6 - fromEnum wu7 + wu8\n  Enum a  Enum b",fontsize=16,color="black",shape="triangle"];108 -> 118[label="",style="solid", color="black", weight=3];
142[label="toEnum0 (primEqInt (Pos (Succ wu900)) (Pos Zero)) (Pos (Succ wu900))",fontsize=16,color="black",shape="box"];142 -> 159[label="",style="solid", color="black", weight=3];
143[label="toEnum0 (primEqInt (Pos Zero) (Pos Zero)) (Pos Zero)",fontsize=16,color="black",shape="box"];143 -> 160[label="",style="solid", color="black", weight=3];
144[label="toEnum0 (primEqInt (Neg (Succ wu900)) (Pos Zero)) (Neg (Succ wu900))",fontsize=16,color="black",shape="box"];144 -> 161[label="",style="solid", color="black", weight=3];
145[label="toEnum0 (primEqInt (Neg Zero) (Pos Zero)) (Neg Zero)",fontsize=16,color="black",shape="box"];145 -> 162[label="",style="solid", color="black", weight=3];
109[label="error []",fontsize=16,color="red",shape="box"];110[label="error []",fontsize=16,color="red",shape="box"];111[label="error []",fontsize=16,color="red",shape="box"];112[label="error []",fontsize=16,color="red",shape="box"];113[label="error []",fontsize=16,color="red",shape="box"];114 -> 119[label="",style="dashed", color="red", weight=0];
114[label="toEnum1 (fromEnum wu6 - fromEnum wu7 + wu8)\n  Enum a  Enum b",fontsize=16,color="magenta"];114 -> 121[label="",style="dashed", color="magenta", weight=3];
115[label="error []",fontsize=16,color="red",shape="box"];116[label="error []",fontsize=16,color="red",shape="box"];117[label="error []",fontsize=16,color="red",shape="box"];118[label="primPlusInt (fromEnum wu6 - fromEnum wu7) wu8\n  Enum a  Enum b",fontsize=16,color="black",shape="box"];118 -> 123[label="",style="solid", color="black", weight=3];
159[label="toEnum0 False (Pos (Succ wu900))",fontsize=16,color="black",shape="box"];159 -> 167[label="",style="solid", color="black", weight=3];
160[label="toEnum0 True (Pos Zero)",fontsize=16,color="black",shape="box"];160 -> 168[label="",style="solid", color="black", weight=3];
161[label="toEnum0 False (Neg (Succ wu900))",fontsize=16,color="black",shape="box"];161 -> 169[label="",style="solid", color="black", weight=3];
162[label="toEnum0 True (Neg Zero)",fontsize=16,color="black",shape="box"];162 -> 170[label="",style="solid", color="black", weight=3];
121 -> 108[label="",style="dashed", color="red", weight=0];
121[label="fromEnum wu6 - fromEnum wu7 + wu8\n  Enum a  Enum b",fontsize=16,color="magenta"];123 -> 125[label="",style="dashed", color="red", weight=0];
123[label="primPlusInt (primMinusInt (fromEnum wu6) (fromEnum wu7)) wu8\n  Enum a  Enum b",fontsize=16,color="magenta"];123 -> 126[label="",style="dashed", color="magenta", weight=3];
123 -> 127[label="",style="dashed", color="magenta", weight=3];
123 -> 128[label="",style="dashed", color="magenta", weight=3];
167[label="error []",fontsize=16,color="red",shape="box"];168[label="()",fontsize=16,color="green",shape="box"];169[label="error []",fontsize=16,color="red",shape="box"];170[label="()",fontsize=16,color="green",shape="box"];126[label="wu7\n  Enum a",fontsize=16,color="green",shape="box"];127[label="wu8",fontsize=16,color="green",shape="box"];128[label="fromEnum wu6\n  Enum a",fontsize=16,color="blue",shape="box"];401[label="fromEnum :: Char -> Int",fontsize=10,color="white",style="solid",shape="box"];128 -> 401[label="",style="solid", color="blue", weight=9];
401 -> 131[label="",style="solid", color="blue", weight=3];
402[label="fromEnum :: Bool -> Int",fontsize=10,color="white",style="solid",shape="box"];128 -> 402[label="",style="solid", color="blue", weight=9];
402 -> 132[label="",style="solid", color="blue", weight=3];
403[label="fromEnum :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];128 -> 403[label="",style="solid", color="blue", weight=9];
403 -> 133[label="",style="solid", color="blue", weight=3];
404[label="fromEnum :: Ordering -> Int",fontsize=10,color="white",style="solid",shape="box"];128 -> 404[label="",style="solid", color="blue", weight=9];
404 -> 134[label="",style="solid", color="blue", weight=3];
405[label="fromEnum :: Integer -> Int",fontsize=10,color="white",style="solid",shape="box"];128 -> 405[label="",style="solid", color="blue", weight=9];
405 -> 135[label="",style="solid", color="blue", weight=3];
406[label="fromEnum :: () -> Int",fontsize=10,color="white",style="solid",shape="box"];128 -> 406[label="",style="solid", color="blue", weight=9];
406 -> 136[label="",style="solid", color="blue", weight=3];
407[label="fromEnum :: Float -> Int",fontsize=10,color="white",style="solid",shape="box"];128 -> 407[label="",style="solid", color="blue", weight=9];
407 -> 137[label="",style="solid", color="blue", weight=3];
408[label="fromEnum :: Double -> Int",fontsize=10,color="white",style="solid",shape="box"];128 -> 408[label="",style="solid", color="blue", weight=9];
408 -> 138[label="",style="solid", color="blue", weight=3];
409[label="fromEnum :: (Ratio a) -> Int",fontsize=10,color="white",style="solid",shape="box"];128 -> 409[label="",style="solid", color="blue", weight=9];
409 -> 139[label="",style="solid", color="blue", weight=3];
125[label="primPlusInt (primMinusInt wu14 (fromEnum wu15)) wu16\n  Enum a",fontsize=16,color="burlywood",shape="triangle"];410[label="wu14/Pos wu140",fontsize=10,color="white",style="solid",shape="box"];125 -> 410[label="",style="solid", color="burlywood", weight=9];
410 -> 140[label="",style="solid", color="burlywood", weight=3];
411[label="wu14/Neg wu140",fontsize=10,color="white",style="solid",shape="box"];125 -> 411[label="",style="solid", color="burlywood", weight=9];
411 -> 141[label="",style="solid", color="burlywood", weight=3];
131[label="fromEnum wu6",fontsize=16,color="black",shape="triangle"];131 -> 146[label="",style="solid", color="black", weight=3];
132[label="fromEnum wu6",fontsize=16,color="black",shape="triangle"];132 -> 147[label="",style="solid", color="black", weight=3];
133[label="fromEnum wu6",fontsize=16,color="black",shape="triangle"];133 -> 148[label="",style="solid", color="black", weight=3];
134[label="fromEnum wu6",fontsize=16,color="black",shape="triangle"];134 -> 149[label="",style="solid", color="black", weight=3];
135[label="fromEnum wu6",fontsize=16,color="black",shape="triangle"];135 -> 150[label="",style="solid", color="black", weight=3];
136 -> 77[label="",style="dashed", color="red", weight=0];
136[label="fromEnum wu6",fontsize=16,color="magenta"];136 -> 151[label="",style="dashed", color="magenta", weight=3];
137[label="fromEnum wu6",fontsize=16,color="black",shape="triangle"];137 -> 152[label="",style="solid", color="black", weight=3];
138[label="fromEnum wu6",fontsize=16,color="black",shape="triangle"];138 -> 153[label="",style="solid", color="black", weight=3];
139[label="fromEnum wu6\n  Integral a",fontsize=16,color="black",shape="triangle"];139 -> 154[label="",style="solid", color="black", weight=3];
140 -> 155[label="",style="dashed", color="red", weight=0];
140[label="primPlusInt (primMinusInt (Pos wu140) (fromEnum wu15)) wu16\n  Enum a",fontsize=16,color="magenta"];140 -> 156[label="",style="dashed", color="magenta", weight=3];
140 -> 157[label="",style="dashed", color="magenta", weight=3];
140 -> 158[label="",style="dashed", color="magenta", weight=3];
141 -> 163[label="",style="dashed", color="red", weight=0];
141[label="primPlusInt (primMinusInt (Neg wu140) (fromEnum wu15)) wu16\n  Enum a",fontsize=16,color="magenta"];141 -> 164[label="",style="dashed", color="magenta", weight=3];
141 -> 165[label="",style="dashed", color="magenta", weight=3];
141 -> 166[label="",style="dashed", color="magenta", weight=3];
146[label="error []",fontsize=16,color="red",shape="box"];147[label="error []",fontsize=16,color="red",shape="box"];148[label="error []",fontsize=16,color="red",shape="box"];149[label="error []",fontsize=16,color="red",shape="box"];150[label="error []",fontsize=16,color="red",shape="box"];151[label="wu6",fontsize=16,color="green",shape="box"];152[label="error []",fontsize=16,color="red",shape="box"];153[label="error []",fontsize=16,color="red",shape="box"];154[label="error []",fontsize=16,color="red",shape="box"];156[label="fromEnum wu15\n  Enum a",fontsize=16,color="blue",shape="box"];415[label="fromEnum :: Char -> Int",fontsize=10,color="white",style="solid",shape="box"];156 -> 415[label="",style="solid", color="blue", weight=9];
415 -> 171[label="",style="solid", color="blue", weight=3];
416[label="fromEnum :: Bool -> Int",fontsize=10,color="white",style="solid",shape="box"];156 -> 416[label="",style="solid", color="blue", weight=9];
416 -> 172[label="",style="solid", color="blue", weight=3];
417[label="fromEnum :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];156 -> 417[label="",style="solid", color="blue", weight=9];
417 -> 173[label="",style="solid", color="blue", weight=3];
418[label="fromEnum :: Ordering -> Int",fontsize=10,color="white",style="solid",shape="box"];156 -> 418[label="",style="solid", color="blue", weight=9];
418 -> 174[label="",style="solid", color="blue", weight=3];
419[label="fromEnum :: Integer -> Int",fontsize=10,color="white",style="solid",shape="box"];156 -> 419[label="",style="solid", color="blue", weight=9];
419 -> 175[label="",style="solid", color="blue", weight=3];
420[label="fromEnum :: () -> Int",fontsize=10,color="white",style="solid",shape="box"];156 -> 420[label="",style="solid", color="blue", weight=9];
420 -> 176[label="",style="solid", color="blue", weight=3];
421[label="fromEnum :: Float -> Int",fontsize=10,color="white",style="solid",shape="box"];156 -> 421[label="",style="solid", color="blue", weight=9];
421 -> 177[label="",style="solid", color="blue", weight=3];
422[label="fromEnum :: Double -> Int",fontsize=10,color="white",style="solid",shape="box"];156 -> 422[label="",style="solid", color="blue", weight=9];
422 -> 178[label="",style="solid", color="blue", weight=3];
423[label="fromEnum :: (Ratio a) -> Int",fontsize=10,color="white",style="solid",shape="box"];156 -> 423[label="",style="solid", color="blue", weight=9];
423 -> 179[label="",style="solid", color="blue", weight=3];
157[label="wu16",fontsize=16,color="green",shape="box"];158[label="wu140",fontsize=16,color="green",shape="box"];155[label="primPlusInt (primMinusInt (Pos wu21) wu22) wu23",fontsize=16,color="burlywood",shape="triangle"];424[label="wu22/Pos wu220",fontsize=10,color="white",style="solid",shape="box"];155 -> 424[label="",style="solid", color="burlywood", weight=9];
424 -> 180[label="",style="solid", color="burlywood", weight=3];
425[label="wu22/Neg wu220",fontsize=10,color="white",style="solid",shape="box"];155 -> 425[label="",style="solid", color="burlywood", weight=9];
425 -> 181[label="",style="solid", color="burlywood", weight=3];
164[label="wu140",fontsize=16,color="green",shape="box"];165[label="fromEnum wu15\n  Enum a",fontsize=16,color="blue",shape="box"];426[label="fromEnum :: Char -> Int",fontsize=10,color="white",style="solid",shape="box"];165 -> 426[label="",style="solid", color="blue", weight=9];
426 -> 182[label="",style="solid", color="blue", weight=3];
427[label="fromEnum :: Bool -> Int",fontsize=10,color="white",style="solid",shape="box"];165 -> 427[label="",style="solid", color="blue", weight=9];
427 -> 183[label="",style="solid", color="blue", weight=3];
428[label="fromEnum :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];165 -> 428[label="",style="solid", color="blue", weight=9];
428 -> 184[label="",style="solid", color="blue", weight=3];
429[label="fromEnum :: Ordering -> Int",fontsize=10,color="white",style="solid",shape="box"];165 -> 429[label="",style="solid", color="blue", weight=9];
429 -> 185[label="",style="solid", color="blue", weight=3];
430[label="fromEnum :: Integer -> Int",fontsize=10,color="white",style="solid",shape="box"];165 -> 430[label="",style="solid", color="blue", weight=9];
430 -> 186[label="",style="solid", color="blue", weight=3];
431[label="fromEnum :: () -> Int",fontsize=10,color="white",style="solid",shape="box"];165 -> 431[label="",style="solid", color="blue", weight=9];
431 -> 187[label="",style="solid", color="blue", weight=3];
432[label="fromEnum :: Float -> Int",fontsize=10,color="white",style="solid",shape="box"];165 -> 432[label="",style="solid", color="blue", weight=9];
432 -> 188[label="",style="solid", color="blue", weight=3];
433[label="fromEnum :: Double -> Int",fontsize=10,color="white",style="solid",shape="box"];165 -> 433[label="",style="solid", color="blue", weight=9];
433 -> 189[label="",style="solid", color="blue", weight=3];
434[label="fromEnum :: (Ratio a) -> Int",fontsize=10,color="white",style="solid",shape="box"];165 -> 434[label="",style="solid", color="blue", weight=9];
434 -> 190[label="",style="solid", color="blue", weight=3];
166[label="wu16",fontsize=16,color="green",shape="box"];163[label="primPlusInt (primMinusInt (Neg wu28) wu29) wu30",fontsize=16,color="burlywood",shape="triangle"];435[label="wu29/Pos wu290",fontsize=10,color="white",style="solid",shape="box"];163 -> 435[label="",style="solid", color="burlywood", weight=9];
435 -> 191[label="",style="solid", color="burlywood", weight=3];
436[label="wu29/Neg wu290",fontsize=10,color="white",style="solid",shape="box"];163 -> 436[label="",style="solid", color="burlywood", weight=9];
436 -> 192[label="",style="solid", color="burlywood", weight=3];
171 -> 131[label="",style="dashed", color="red", weight=0];
171[label="fromEnum wu15",fontsize=16,color="magenta"];171 -> 193[label="",style="dashed", color="magenta", weight=3];
172 -> 132[label="",style="dashed", color="red", weight=0];
172[label="fromEnum wu15",fontsize=16,color="magenta"];172 -> 194[label="",style="dashed", color="magenta", weight=3];
173 -> 133[label="",style="dashed", color="red", weight=0];
173[label="fromEnum wu15",fontsize=16,color="magenta"];173 -> 195[label="",style="dashed", color="magenta", weight=3];
174 -> 134[label="",style="dashed", color="red", weight=0];
174[label="fromEnum wu15",fontsize=16,color="magenta"];174 -> 196[label="",style="dashed", color="magenta", weight=3];
175 -> 135[label="",style="dashed", color="red", weight=0];
175[label="fromEnum wu15",fontsize=16,color="magenta"];175 -> 197[label="",style="dashed", color="magenta", weight=3];
176 -> 77[label="",style="dashed", color="red", weight=0];
176[label="fromEnum wu15",fontsize=16,color="magenta"];176 -> 198[label="",style="dashed", color="magenta", weight=3];
177 -> 137[label="",style="dashed", color="red", weight=0];
177[label="fromEnum wu15",fontsize=16,color="magenta"];177 -> 199[label="",style="dashed", color="magenta", weight=3];
178 -> 138[label="",style="dashed", color="red", weight=0];
178[label="fromEnum wu15",fontsize=16,color="magenta"];178 -> 200[label="",style="dashed", color="magenta", weight=3];
179 -> 139[label="",style="dashed", color="red", weight=0];
179[label="fromEnum wu15\n  Integral a",fontsize=16,color="magenta"];179 -> 201[label="",style="dashed", color="magenta", weight=3];
180[label="primPlusInt (primMinusInt (Pos wu21) (Pos wu220)) wu23",fontsize=16,color="black",shape="box"];180 -> 202[label="",style="solid", color="black", weight=3];
181[label="primPlusInt (primMinusInt (Pos wu21) (Neg wu220)) wu23",fontsize=16,color="black",shape="box"];181 -> 203[label="",style="solid", color="black", weight=3];
182 -> 131[label="",style="dashed", color="red", weight=0];
182[label="fromEnum wu15",fontsize=16,color="magenta"];182 -> 204[label="",style="dashed", color="magenta", weight=3];
183 -> 132[label="",style="dashed", color="red", weight=0];
183[label="fromEnum wu15",fontsize=16,color="magenta"];183 -> 205[label="",style="dashed", color="magenta", weight=3];
184 -> 133[label="",style="dashed", color="red", weight=0];
184[label="fromEnum wu15",fontsize=16,color="magenta"];184 -> 206[label="",style="dashed", color="magenta", weight=3];
185 -> 134[label="",style="dashed", color="red", weight=0];
185[label="fromEnum wu15",fontsize=16,color="magenta"];185 -> 207[label="",style="dashed", color="magenta", weight=3];
186 -> 135[label="",style="dashed", color="red", weight=0];
186[label="fromEnum wu15",fontsize=16,color="magenta"];186 -> 208[label="",style="dashed", color="magenta", weight=3];
187 -> 77[label="",style="dashed", color="red", weight=0];
187[label="fromEnum wu15",fontsize=16,color="magenta"];187 -> 209[label="",style="dashed", color="magenta", weight=3];
188 -> 137[label="",style="dashed", color="red", weight=0];
188[label="fromEnum wu15",fontsize=16,color="magenta"];188 -> 210[label="",style="dashed", color="magenta", weight=3];
189 -> 138[label="",style="dashed", color="red", weight=0];
189[label="fromEnum wu15",fontsize=16,color="magenta"];189 -> 211[label="",style="dashed", color="magenta", weight=3];
190 -> 139[label="",style="dashed", color="red", weight=0];
190[label="fromEnum wu15\n  Integral a",fontsize=16,color="magenta"];190 -> 212[label="",style="dashed", color="magenta", weight=3];
191[label="primPlusInt (primMinusInt (Neg wu28) (Pos wu290)) wu30",fontsize=16,color="black",shape="box"];191 -> 213[label="",style="solid", color="black", weight=3];
192[label="primPlusInt (primMinusInt (Neg wu28) (Neg wu290)) wu30",fontsize=16,color="black",shape="box"];192 -> 214[label="",style="solid", color="black", weight=3];
193[label="wu15",fontsize=16,color="green",shape="box"];194[label="wu15",fontsize=16,color="green",shape="box"];195[label="wu15",fontsize=16,color="green",shape="box"];196[label="wu15",fontsize=16,color="green",shape="box"];197[label="wu15",fontsize=16,color="green",shape="box"];198[label="wu15",fontsize=16,color="green",shape="box"];199[label="wu15",fontsize=16,color="green",shape="box"];200[label="wu15",fontsize=16,color="green",shape="box"];201[label="wu15\n  Integral a",fontsize=16,color="green",shape="box"];202[label="primPlusInt (primMinusNat wu21 wu220) wu23",fontsize=16,color="burlywood",shape="triangle"];455[label="wu21/Succ wu210",fontsize=10,color="white",style="solid",shape="box"];202 -> 455[label="",style="solid", color="burlywood", weight=9];
455 -> 215[label="",style="solid", color="burlywood", weight=3];
456[label="wu21/Zero",fontsize=10,color="white",style="solid",shape="box"];202 -> 456[label="",style="solid", color="burlywood", weight=9];
456 -> 216[label="",style="solid", color="burlywood", weight=3];
203[label="primPlusInt (Pos (primPlusNat wu21 wu220)) wu23",fontsize=16,color="burlywood",shape="box"];457[label="wu23/Pos wu230",fontsize=10,color="white",style="solid",shape="box"];203 -> 457[label="",style="solid", color="burlywood", weight=9];
457 -> 217[label="",style="solid", color="burlywood", weight=3];
458[label="wu23/Neg wu230",fontsize=10,color="white",style="solid",shape="box"];203 -> 458[label="",style="solid", color="burlywood", weight=9];
458 -> 218[label="",style="solid", color="burlywood", weight=3];
204[label="wu15",fontsize=16,color="green",shape="box"];205[label="wu15",fontsize=16,color="green",shape="box"];206[label="wu15",fontsize=16,color="green",shape="box"];207[label="wu15",fontsize=16,color="green",shape="box"];208[label="wu15",fontsize=16,color="green",shape="box"];209[label="wu15",fontsize=16,color="green",shape="box"];210[label="wu15",fontsize=16,color="green",shape="box"];211[label="wu15",fontsize=16,color="green",shape="box"];212[label="wu15\n  Integral a",fontsize=16,color="green",shape="box"];213[label="primPlusInt (Neg (primPlusNat wu28 wu290)) wu30",fontsize=16,color="burlywood",shape="box"];459[label="wu30/Pos wu300",fontsize=10,color="white",style="solid",shape="box"];213 -> 459[label="",style="solid", color="burlywood", weight=9];
459 -> 219[label="",style="solid", color="burlywood", weight=3];
460[label="wu30/Neg wu300",fontsize=10,color="white",style="solid",shape="box"];213 -> 460[label="",style="solid", color="burlywood", weight=9];
460 -> 220[label="",style="solid", color="burlywood", weight=3];
214 -> 202[label="",style="dashed", color="red", weight=0];
214[label="primPlusInt (primMinusNat wu290 wu28) wu30",fontsize=16,color="magenta"];214 -> 221[label="",style="dashed", color="magenta", weight=3];
214 -> 222[label="",style="dashed", color="magenta", weight=3];
214 -> 223[label="",style="dashed", color="magenta", weight=3];
215[label="primPlusInt (primMinusNat (Succ wu210) wu220) wu23",fontsize=16,color="burlywood",shape="box"];462[label="wu220/Succ wu2200",fontsize=10,color="white",style="solid",shape="box"];215 -> 462[label="",style="solid", color="burlywood", weight=9];
462 -> 224[label="",style="solid", color="burlywood", weight=3];
463[label="wu220/Zero",fontsize=10,color="white",style="solid",shape="box"];215 -> 463[label="",style="solid", color="burlywood", weight=9];
463 -> 225[label="",style="solid", color="burlywood", weight=3];
216[label="primPlusInt (primMinusNat Zero wu220) wu23",fontsize=16,color="burlywood",shape="box"];464[label="wu220/Succ wu2200",fontsize=10,color="white",style="solid",shape="box"];216 -> 464[label="",style="solid", color="burlywood", weight=9];
464 -> 226[label="",style="solid", color="burlywood", weight=3];
465[label="wu220/Zero",fontsize=10,color="white",style="solid",shape="box"];216 -> 465[label="",style="solid", color="burlywood", weight=9];
465 -> 227[label="",style="solid", color="burlywood", weight=3];
217[label="primPlusInt (Pos (primPlusNat wu21 wu220)) (Pos wu230)",fontsize=16,color="black",shape="box"];217 -> 228[label="",style="solid", color="black", weight=3];
218[label="primPlusInt (Pos (primPlusNat wu21 wu220)) (Neg wu230)",fontsize=16,color="black",shape="box"];218 -> 229[label="",style="solid", color="black", weight=3];
219[label="primPlusInt (Neg (primPlusNat wu28 wu290)) (Pos wu300)",fontsize=16,color="black",shape="box"];219 -> 230[label="",style="solid", color="black", weight=3];
220[label="primPlusInt (Neg (primPlusNat wu28 wu290)) (Neg wu300)",fontsize=16,color="black",shape="box"];220 -> 231[label="",style="solid", color="black", weight=3];
221[label="wu30",fontsize=16,color="green",shape="box"];222[label="wu28",fontsize=16,color="green",shape="box"];223[label="wu290",fontsize=16,color="green",shape="box"];224[label="primPlusInt (primMinusNat (Succ wu210) (Succ wu2200)) wu23",fontsize=16,color="black",shape="box"];224 -> 232[label="",style="solid", color="black", weight=3];
225[label="primPlusInt (primMinusNat (Succ wu210) Zero) wu23",fontsize=16,color="black",shape="box"];225 -> 233[label="",style="solid", color="black", weight=3];
226[label="primPlusInt (primMinusNat Zero (Succ wu2200)) wu23",fontsize=16,color="black",shape="box"];226 -> 234[label="",style="solid", color="black", weight=3];
227[label="primPlusInt (primMinusNat Zero Zero) wu23",fontsize=16,color="black",shape="box"];227 -> 235[label="",style="solid", color="black", weight=3];
228[label="Pos (primPlusNat (primPlusNat wu21 wu220) wu230)",fontsize=16,color="green",shape="box"];228 -> 236[label="",style="dashed", color="green", weight=3];
229[label="primMinusNat (primPlusNat wu21 wu220) wu230",fontsize=16,color="burlywood",shape="box"];466[label="wu21/Succ wu210",fontsize=10,color="white",style="solid",shape="box"];229 -> 466[label="",style="solid", color="burlywood", weight=9];
466 -> 237[label="",style="solid", color="burlywood", weight=3];
467[label="wu21/Zero",fontsize=10,color="white",style="solid",shape="box"];229 -> 467[label="",style="solid", color="burlywood", weight=9];
467 -> 238[label="",style="solid", color="burlywood", weight=3];
230[label="primMinusNat wu300 (primPlusNat wu28 wu290)",fontsize=16,color="burlywood",shape="box"];468[label="wu300/Succ wu3000",fontsize=10,color="white",style="solid",shape="box"];230 -> 468[label="",style="solid", color="burlywood", weight=9];
468 -> 239[label="",style="solid", color="burlywood", weight=3];
469[label="wu300/Zero",fontsize=10,color="white",style="solid",shape="box"];230 -> 469[label="",style="solid", color="burlywood", weight=9];
469 -> 240[label="",style="solid", color="burlywood", weight=3];
231[label="Neg (primPlusNat (primPlusNat wu28 wu290) wu300)",fontsize=16,color="green",shape="box"];231 -> 241[label="",style="dashed", color="green", weight=3];
232 -> 202[label="",style="dashed", color="red", weight=0];
232[label="primPlusInt (primMinusNat wu210 wu2200) wu23",fontsize=16,color="magenta"];232 -> 242[label="",style="dashed", color="magenta", weight=3];
232 -> 243[label="",style="dashed", color="magenta", weight=3];
233[label="primPlusInt (Pos (Succ wu210)) wu23",fontsize=16,color="burlywood",shape="box"];471[label="wu23/Pos wu230",fontsize=10,color="white",style="solid",shape="box"];233 -> 471[label="",style="solid", color="burlywood", weight=9];
471 -> 244[label="",style="solid", color="burlywood", weight=3];
472[label="wu23/Neg wu230",fontsize=10,color="white",style="solid",shape="box"];233 -> 472[label="",style="solid", color="burlywood", weight=9];
472 -> 245[label="",style="solid", color="burlywood", weight=3];
234[label="primPlusInt (Neg (Succ wu2200)) wu23",fontsize=16,color="burlywood",shape="box"];473[label="wu23/Pos wu230",fontsize=10,color="white",style="solid",shape="box"];234 -> 473[label="",style="solid", color="burlywood", weight=9];
473 -> 246[label="",style="solid", color="burlywood", weight=3];
474[label="wu23/Neg wu230",fontsize=10,color="white",style="solid",shape="box"];234 -> 474[label="",style="solid", color="burlywood", weight=9];
474 -> 247[label="",style="solid", color="burlywood", weight=3];
235[label="primPlusInt (Pos Zero) wu23",fontsize=16,color="burlywood",shape="box"];475[label="wu23/Pos wu230",fontsize=10,color="white",style="solid",shape="box"];235 -> 475[label="",style="solid", color="burlywood", weight=9];
475 -> 248[label="",style="solid", color="burlywood", weight=3];
476[label="wu23/Neg wu230",fontsize=10,color="white",style="solid",shape="box"];235 -> 476[label="",style="solid", color="burlywood", weight=9];
476 -> 249[label="",style="solid", color="burlywood", weight=3];
236[label="primPlusNat (primPlusNat wu21 wu220) wu230",fontsize=16,color="burlywood",shape="triangle"];477[label="wu21/Succ wu210",fontsize=10,color="white",style="solid",shape="box"];236 -> 477[label="",style="solid", color="burlywood", weight=9];
477 -> 250[label="",style="solid", color="burlywood", weight=3];
478[label="wu21/Zero",fontsize=10,color="white",style="solid",shape="box"];236 -> 478[label="",style="solid", color="burlywood", weight=9];
478 -> 251[label="",style="solid", color="burlywood", weight=3];
237[label="primMinusNat (primPlusNat (Succ wu210) wu220) wu230",fontsize=16,color="burlywood",shape="box"];479[label="wu220/Succ wu2200",fontsize=10,color="white",style="solid",shape="box"];237 -> 479[label="",style="solid", color="burlywood", weight=9];
479 -> 252[label="",style="solid", color="burlywood", weight=3];
480[label="wu220/Zero",fontsize=10,color="white",style="solid",shape="box"];237 -> 480[label="",style="solid", color="burlywood", weight=9];
480 -> 253[label="",style="solid", color="burlywood", weight=3];
238[label="primMinusNat (primPlusNat Zero wu220) wu230",fontsize=16,color="burlywood",shape="box"];481[label="wu220/Succ wu2200",fontsize=10,color="white",style="solid",shape="box"];238 -> 481[label="",style="solid", color="burlywood", weight=9];
481 -> 254[label="",style="solid", color="burlywood", weight=3];
482[label="wu220/Zero",fontsize=10,color="white",style="solid",shape="box"];238 -> 482[label="",style="solid", color="burlywood", weight=9];
482 -> 255[label="",style="solid", color="burlywood", weight=3];
239[label="primMinusNat (Succ wu3000) (primPlusNat wu28 wu290)",fontsize=16,color="burlywood",shape="box"];483[label="wu28/Succ wu280",fontsize=10,color="white",style="solid",shape="box"];239 -> 483[label="",style="solid", color="burlywood", weight=9];
483 -> 256[label="",style="solid", color="burlywood", weight=3];
484[label="wu28/Zero",fontsize=10,color="white",style="solid",shape="box"];239 -> 484[label="",style="solid", color="burlywood", weight=9];
484 -> 257[label="",style="solid", color="burlywood", weight=3];
240[label="primMinusNat Zero (primPlusNat wu28 wu290)",fontsize=16,color="burlywood",shape="box"];485[label="wu28/Succ wu280",fontsize=10,color="white",style="solid",shape="box"];240 -> 485[label="",style="solid", color="burlywood", weight=9];
485 -> 258[label="",style="solid", color="burlywood", weight=3];
486[label="wu28/Zero",fontsize=10,color="white",style="solid",shape="box"];240 -> 486[label="",style="solid", color="burlywood", weight=9];
486 -> 259[label="",style="solid", color="burlywood", weight=3];
241 -> 236[label="",style="dashed", color="red", weight=0];
241[label="primPlusNat (primPlusNat wu28 wu290) wu300",fontsize=16,color="magenta"];241 -> 260[label="",style="dashed", color="magenta", weight=3];
241 -> 261[label="",style="dashed", color="magenta", weight=3];
241 -> 262[label="",style="dashed", color="magenta", weight=3];
242[label="wu2200",fontsize=16,color="green",shape="box"];243[label="wu210",fontsize=16,color="green",shape="box"];244[label="primPlusInt (Pos (Succ wu210)) (Pos wu230)",fontsize=16,color="black",shape="box"];244 -> 263[label="",style="solid", color="black", weight=3];
245[label="primPlusInt (Pos (Succ wu210)) (Neg wu230)",fontsize=16,color="black",shape="box"];245 -> 264[label="",style="solid", color="black", weight=3];
246[label="primPlusInt (Neg (Succ wu2200)) (Pos wu230)",fontsize=16,color="black",shape="box"];246 -> 265[label="",style="solid", color="black", weight=3];
247[label="primPlusInt (Neg (Succ wu2200)) (Neg wu230)",fontsize=16,color="black",shape="box"];247 -> 266[label="",style="solid", color="black", weight=3];
248[label="primPlusInt (Pos Zero) (Pos wu230)",fontsize=16,color="black",shape="box"];248 -> 267[label="",style="solid", color="black", weight=3];
249[label="primPlusInt (Pos Zero) (Neg wu230)",fontsize=16,color="black",shape="box"];249 -> 268[label="",style="solid", color="black", weight=3];
250[label="primPlusNat (primPlusNat (Succ wu210) wu220) wu230",fontsize=16,color="burlywood",shape="box"];488[label="wu220/Succ wu2200",fontsize=10,color="white",style="solid",shape="box"];250 -> 488[label="",style="solid", color="burlywood", weight=9];
488 -> 269[label="",style="solid", color="burlywood", weight=3];
489[label="wu220/Zero",fontsize=10,color="white",style="solid",shape="box"];250 -> 489[label="",style="solid", color="burlywood", weight=9];
489 -> 270[label="",style="solid", color="burlywood", weight=3];
251[label="primPlusNat (primPlusNat Zero wu220) wu230",fontsize=16,color="burlywood",shape="box"];490[label="wu220/Succ wu2200",fontsize=10,color="white",style="solid",shape="box"];251 -> 490[label="",style="solid", color="burlywood", weight=9];
490 -> 271[label="",style="solid", color="burlywood", weight=3];
491[label="wu220/Zero",fontsize=10,color="white",style="solid",shape="box"];251 -> 491[label="",style="solid", color="burlywood", weight=9];
491 -> 272[label="",style="solid", color="burlywood", weight=3];
252[label="primMinusNat (primPlusNat (Succ wu210) (Succ wu2200)) wu230",fontsize=16,color="black",shape="box"];252 -> 273[label="",style="solid", color="black", weight=3];
253[label="primMinusNat (primPlusNat (Succ wu210) Zero) wu230",fontsize=16,color="black",shape="box"];253 -> 274[label="",style="solid", color="black", weight=3];
254[label="primMinusNat (primPlusNat Zero (Succ wu2200)) wu230",fontsize=16,color="black",shape="box"];254 -> 275[label="",style="solid", color="black", weight=3];
255[label="primMinusNat (primPlusNat Zero Zero) wu230",fontsize=16,color="black",shape="box"];255 -> 276[label="",style="solid", color="black", weight=3];
256[label="primMinusNat (Succ wu3000) (primPlusNat (Succ wu280) wu290)",fontsize=16,color="burlywood",shape="box"];492[label="wu290/Succ wu2900",fontsize=10,color="white",style="solid",shape="box"];256 -> 492[label="",style="solid", color="burlywood", weight=9];
492 -> 277[label="",style="solid", color="burlywood", weight=3];
493[label="wu290/Zero",fontsize=10,color="white",style="solid",shape="box"];256 -> 493[label="",style="solid", color="burlywood", weight=9];
493 -> 278[label="",style="solid", color="burlywood", weight=3];
257[label="primMinusNat (Succ wu3000) (primPlusNat Zero wu290)",fontsize=16,color="burlywood",shape="box"];494[label="wu290/Succ wu2900",fontsize=10,color="white",style="solid",shape="box"];257 -> 494[label="",style="solid", color="burlywood", weight=9];
494 -> 279[label="",style="solid", color="burlywood", weight=3];
495[label="wu290/Zero",fontsize=10,color="white",style="solid",shape="box"];257 -> 495[label="",style="solid", color="burlywood", weight=9];
495 -> 280[label="",style="solid", color="burlywood", weight=3];
258[label="primMinusNat Zero (primPlusNat (Succ wu280) wu290)",fontsize=16,color="burlywood",shape="box"];496[label="wu290/Succ wu2900",fontsize=10,color="white",style="solid",shape="box"];258 -> 496[label="",style="solid", color="burlywood", weight=9];
496 -> 281[label="",style="solid", color="burlywood", weight=3];
497[label="wu290/Zero",fontsize=10,color="white",style="solid",shape="box"];258 -> 497[label="",style="solid", color="burlywood", weight=9];
497 -> 282[label="",style="solid", color="burlywood", weight=3];
259[label="primMinusNat Zero (primPlusNat Zero wu290)",fontsize=16,color="burlywood",shape="box"];498[label="wu290/Succ wu2900",fontsize=10,color="white",style="solid",shape="box"];259 -> 498[label="",style="solid", color="burlywood", weight=9];
498 -> 283[label="",style="solid", color="burlywood", weight=3];
499[label="wu290/Zero",fontsize=10,color="white",style="solid",shape="box"];259 -> 499[label="",style="solid", color="burlywood", weight=9];
499 -> 284[label="",style="solid", color="burlywood", weight=3];
260[label="wu290",fontsize=16,color="green",shape="box"];261[label="wu300",fontsize=16,color="green",shape="box"];262[label="wu28",fontsize=16,color="green",shape="box"];263[label="Pos (primPlusNat (Succ wu210) wu230)",fontsize=16,color="green",shape="box"];263 -> 285[label="",style="dashed", color="green", weight=3];
264[label="primMinusNat (Succ wu210) wu230",fontsize=16,color="burlywood",shape="triangle"];500[label="wu230/Succ wu2300",fontsize=10,color="white",style="solid",shape="box"];264 -> 500[label="",style="solid", color="burlywood", weight=9];
500 -> 286[label="",style="solid", color="burlywood", weight=3];
501[label="wu230/Zero",fontsize=10,color="white",style="solid",shape="box"];264 -> 501[label="",style="solid", color="burlywood", weight=9];
501 -> 287[label="",style="solid", color="burlywood", weight=3];
265[label="primMinusNat wu230 (Succ wu2200)",fontsize=16,color="burlywood",shape="triangle"];502[label="wu230/Succ wu2300",fontsize=10,color="white",style="solid",shape="box"];265 -> 502[label="",style="solid", color="burlywood", weight=9];
502 -> 288[label="",style="solid", color="burlywood", weight=3];
503[label="wu230/Zero",fontsize=10,color="white",style="solid",shape="box"];265 -> 503[label="",style="solid", color="burlywood", weight=9];
503 -> 289[label="",style="solid", color="burlywood", weight=3];
266[label="Neg (primPlusNat (Succ wu2200) wu230)",fontsize=16,color="green",shape="box"];266 -> 290[label="",style="dashed", color="green", weight=3];
267[label="Pos (primPlusNat Zero wu230)",fontsize=16,color="green",shape="box"];267 -> 291[label="",style="dashed", color="green", weight=3];
268[label="primMinusNat Zero wu230",fontsize=16,color="burlywood",shape="triangle"];504[label="wu230/Succ wu2300",fontsize=10,color="white",style="solid",shape="box"];268 -> 504[label="",style="solid", color="burlywood", weight=9];
504 -> 292[label="",style="solid", color="burlywood", weight=3];
505[label="wu230/Zero",fontsize=10,color="white",style="solid",shape="box"];268 -> 505[label="",style="solid", color="burlywood", weight=9];
505 -> 293[label="",style="solid", color="burlywood", weight=3];
269[label="primPlusNat (primPlusNat (Succ wu210) (Succ wu2200)) wu230",fontsize=16,color="black",shape="box"];269 -> 294[label="",style="solid", color="black", weight=3];
270[label="primPlusNat (primPlusNat (Succ wu210) Zero) wu230",fontsize=16,color="black",shape="box"];270 -> 295[label="",style="solid", color="black", weight=3];
271[label="primPlusNat (primPlusNat Zero (Succ wu2200)) wu230",fontsize=16,color="black",shape="box"];271 -> 296[label="",style="solid", color="black", weight=3];
272[label="primPlusNat (primPlusNat Zero Zero) wu230",fontsize=16,color="black",shape="box"];272 -> 297[label="",style="solid", color="black", weight=3];
273 -> 264[label="",style="dashed", color="red", weight=0];
273[label="primMinusNat (Succ (Succ (primPlusNat wu210 wu2200))) wu230",fontsize=16,color="magenta"];273 -> 298[label="",style="dashed", color="magenta", weight=3];
274 -> 264[label="",style="dashed", color="red", weight=0];
274[label="primMinusNat (Succ wu210) wu230",fontsize=16,color="magenta"];275 -> 264[label="",style="dashed", color="red", weight=0];
275[label="primMinusNat (Succ wu2200) wu230",fontsize=16,color="magenta"];275 -> 299[label="",style="dashed", color="magenta", weight=3];
276 -> 268[label="",style="dashed", color="red", weight=0];
276[label="primMinusNat Zero wu230",fontsize=16,color="magenta"];277[label="primMinusNat (Succ wu3000) (primPlusNat (Succ wu280) (Succ wu2900))",fontsize=16,color="black",shape="box"];277 -> 300[label="",style="solid", color="black", weight=3];
278[label="primMinusNat (Succ wu3000) (primPlusNat (Succ wu280) Zero)",fontsize=16,color="black",shape="box"];278 -> 301[label="",style="solid", color="black", weight=3];
279[label="primMinusNat (Succ wu3000) (primPlusNat Zero (Succ wu2900))",fontsize=16,color="black",shape="box"];279 -> 302[label="",style="solid", color="black", weight=3];
280[label="primMinusNat (Succ wu3000) (primPlusNat Zero Zero)",fontsize=16,color="black",shape="box"];280 -> 303[label="",style="solid", color="black", weight=3];
281[label="primMinusNat Zero (primPlusNat (Succ wu280) (Succ wu2900))",fontsize=16,color="black",shape="box"];281 -> 304[label="",style="solid", color="black", weight=3];
282[label="primMinusNat Zero (primPlusNat (Succ wu280) Zero)",fontsize=16,color="black",shape="box"];282 -> 305[label="",style="solid", color="black", weight=3];
283[label="primMinusNat Zero (primPlusNat Zero (Succ wu2900))",fontsize=16,color="black",shape="box"];283 -> 306[label="",style="solid", color="black", weight=3];
284[label="primMinusNat Zero (primPlusNat Zero Zero)",fontsize=16,color="black",shape="box"];284 -> 307[label="",style="solid", color="black", weight=3];
285[label="primPlusNat (Succ wu210) wu230",fontsize=16,color="burlywood",shape="triangle"];510[label="wu230/Succ wu2300",fontsize=10,color="white",style="solid",shape="box"];285 -> 510[label="",style="solid", color="burlywood", weight=9];
510 -> 308[label="",style="solid", color="burlywood", weight=3];
511[label="wu230/Zero",fontsize=10,color="white",style="solid",shape="box"];285 -> 511[label="",style="solid", color="burlywood", weight=9];
511 -> 309[label="",style="solid", color="burlywood", weight=3];
286[label="primMinusNat (Succ wu210) (Succ wu2300)",fontsize=16,color="black",shape="box"];286 -> 310[label="",style="solid", color="black", weight=3];
287[label="primMinusNat (Succ wu210) Zero",fontsize=16,color="black",shape="box"];287 -> 311[label="",style="solid", color="black", weight=3];
288[label="primMinusNat (Succ wu2300) (Succ wu2200)",fontsize=16,color="black",shape="box"];288 -> 312[label="",style="solid", color="black", weight=3];
289[label="primMinusNat Zero (Succ wu2200)",fontsize=16,color="black",shape="box"];289 -> 313[label="",style="solid", color="black", weight=3];
290 -> 285[label="",style="dashed", color="red", weight=0];
290[label="primPlusNat (Succ wu2200) wu230",fontsize=16,color="magenta"];290 -> 314[label="",style="dashed", color="magenta", weight=3];
290 -> 315[label="",style="dashed", color="magenta", weight=3];
291[label="primPlusNat Zero wu230",fontsize=16,color="burlywood",shape="triangle"];513[label="wu230/Succ wu2300",fontsize=10,color="white",style="solid",shape="box"];291 -> 513[label="",style="solid", color="burlywood", weight=9];
513 -> 316[label="",style="solid", color="burlywood", weight=3];
514[label="wu230/Zero",fontsize=10,color="white",style="solid",shape="box"];291 -> 514[label="",style="solid", color="burlywood", weight=9];
514 -> 317[label="",style="solid", color="burlywood", weight=3];
292[label="primMinusNat Zero (Succ wu2300)",fontsize=16,color="black",shape="box"];292 -> 318[label="",style="solid", color="black", weight=3];
293[label="primMinusNat Zero Zero",fontsize=16,color="black",shape="box"];293 -> 319[label="",style="solid", color="black", weight=3];
294 -> 285[label="",style="dashed", color="red", weight=0];
294[label="primPlusNat (Succ (Succ (primPlusNat wu210 wu2200))) wu230",fontsize=16,color="magenta"];294 -> 320[label="",style="dashed", color="magenta", weight=3];
295 -> 285[label="",style="dashed", color="red", weight=0];
295[label="primPlusNat (Succ wu210) wu230",fontsize=16,color="magenta"];296 -> 285[label="",style="dashed", color="red", weight=0];
296[label="primPlusNat (Succ wu2200) wu230",fontsize=16,color="magenta"];296 -> 321[label="",style="dashed", color="magenta", weight=3];
297 -> 291[label="",style="dashed", color="red", weight=0];
297[label="primPlusNat Zero wu230",fontsize=16,color="magenta"];298[label="Succ (primPlusNat wu210 wu2200)",fontsize=16,color="green",shape="box"];298 -> 322[label="",style="dashed", color="green", weight=3];
299[label="wu2200",fontsize=16,color="green",shape="box"];300 -> 265[label="",style="dashed", color="red", weight=0];
300[label="primMinusNat (Succ wu3000) (Succ (Succ (primPlusNat wu280 wu2900)))",fontsize=16,color="magenta"];300 -> 323[label="",style="dashed", color="magenta", weight=3];
300 -> 324[label="",style="dashed", color="magenta", weight=3];
301 -> 265[label="",style="dashed", color="red", weight=0];
301[label="primMinusNat (Succ wu3000) (Succ wu280)",fontsize=16,color="magenta"];301 -> 325[label="",style="dashed", color="magenta", weight=3];
301 -> 326[label="",style="dashed", color="magenta", weight=3];
302 -> 265[label="",style="dashed", color="red", weight=0];
302[label="primMinusNat (Succ wu3000) (Succ wu2900)",fontsize=16,color="magenta"];302 -> 327[label="",style="dashed", color="magenta", weight=3];
302 -> 328[label="",style="dashed", color="magenta", weight=3];
303 -> 264[label="",style="dashed", color="red", weight=0];
303[label="primMinusNat (Succ wu3000) Zero",fontsize=16,color="magenta"];303 -> 329[label="",style="dashed", color="magenta", weight=3];
303 -> 330[label="",style="dashed", color="magenta", weight=3];
304 -> 265[label="",style="dashed", color="red", weight=0];
304[label="primMinusNat Zero (Succ (Succ (primPlusNat wu280 wu2900)))",fontsize=16,color="magenta"];304 -> 331[label="",style="dashed", color="magenta", weight=3];
304 -> 332[label="",style="dashed", color="magenta", weight=3];
305 -> 265[label="",style="dashed", color="red", weight=0];
305[label="primMinusNat Zero (Succ wu280)",fontsize=16,color="magenta"];305 -> 333[label="",style="dashed", color="magenta", weight=3];
305 -> 334[label="",style="dashed", color="magenta", weight=3];
306 -> 265[label="",style="dashed", color="red", weight=0];
306[label="primMinusNat Zero (Succ wu2900)",fontsize=16,color="magenta"];306 -> 335[label="",style="dashed", color="magenta", weight=3];
306 -> 336[label="",style="dashed", color="magenta", weight=3];
307 -> 268[label="",style="dashed", color="red", weight=0];
307[label="primMinusNat Zero Zero",fontsize=16,color="magenta"];307 -> 337[label="",style="dashed", color="magenta", weight=3];
308[label="primPlusNat (Succ wu210) (Succ wu2300)",fontsize=16,color="black",shape="box"];308 -> 338[label="",style="solid", color="black", weight=3];
309[label="primPlusNat (Succ wu210) Zero",fontsize=16,color="black",shape="box"];309 -> 339[label="",style="solid", color="black", weight=3];
310[label="primMinusNat wu210 wu2300",fontsize=16,color="burlywood",shape="triangle"];527[label="wu210/Succ wu2100",fontsize=10,color="white",style="solid",shape="box"];310 -> 527[label="",style="solid", color="burlywood", weight=9];
527 -> 340[label="",style="solid", color="burlywood", weight=3];
528[label="wu210/Zero",fontsize=10,color="white",style="solid",shape="box"];310 -> 528[label="",style="solid", color="burlywood", weight=9];
528 -> 341[label="",style="solid", color="burlywood", weight=3];
311[label="Pos (Succ wu210)",fontsize=16,color="green",shape="box"];312 -> 310[label="",style="dashed", color="red", weight=0];
312[label="primMinusNat wu2300 wu2200",fontsize=16,color="magenta"];312 -> 342[label="",style="dashed", color="magenta", weight=3];
312 -> 343[label="",style="dashed", color="magenta", weight=3];
313[label="Neg (Succ wu2200)",fontsize=16,color="green",shape="box"];314[label="wu230",fontsize=16,color="green",shape="box"];315[label="wu2200",fontsize=16,color="green",shape="box"];316[label="primPlusNat Zero (Succ wu2300)",fontsize=16,color="black",shape="box"];316 -> 344[label="",style="solid", color="black", weight=3];
317[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];317 -> 345[label="",style="solid", color="black", weight=3];
318[label="Neg (Succ wu2300)",fontsize=16,color="green",shape="box"];319[label="Pos Zero",fontsize=16,color="green",shape="box"];320[label="Succ (primPlusNat wu210 wu2200)",fontsize=16,color="green",shape="box"];320 -> 346[label="",style="dashed", color="green", weight=3];
321[label="wu2200",fontsize=16,color="green",shape="box"];322[label="primPlusNat wu210 wu2200",fontsize=16,color="burlywood",shape="triangle"];530[label="wu210/Succ wu2100",fontsize=10,color="white",style="solid",shape="box"];322 -> 530[label="",style="solid", color="burlywood", weight=9];
530 -> 347[label="",style="solid", color="burlywood", weight=3];
531[label="wu210/Zero",fontsize=10,color="white",style="solid",shape="box"];322 -> 531[label="",style="solid", color="burlywood", weight=9];
531 -> 348[label="",style="solid", color="burlywood", weight=3];
323[label="Succ wu3000",fontsize=16,color="green",shape="box"];324[label="Succ (primPlusNat wu280 wu2900)",fontsize=16,color="green",shape="box"];324 -> 349[label="",style="dashed", color="green", weight=3];
325[label="Succ wu3000",fontsize=16,color="green",shape="box"];326[label="wu280",fontsize=16,color="green",shape="box"];327[label="Succ wu3000",fontsize=16,color="green",shape="box"];328[label="wu2900",fontsize=16,color="green",shape="box"];329[label="Zero",fontsize=16,color="green",shape="box"];330[label="wu3000",fontsize=16,color="green",shape="box"];331[label="Zero",fontsize=16,color="green",shape="box"];332[label="Succ (primPlusNat wu280 wu2900)",fontsize=16,color="green",shape="box"];332 -> 350[label="",style="dashed", color="green", weight=3];
333[label="Zero",fontsize=16,color="green",shape="box"];334[label="wu280",fontsize=16,color="green",shape="box"];335[label="Zero",fontsize=16,color="green",shape="box"];336[label="wu2900",fontsize=16,color="green",shape="box"];337[label="Zero",fontsize=16,color="green",shape="box"];338[label="Succ (Succ (primPlusNat wu210 wu2300))",fontsize=16,color="green",shape="box"];338 -> 351[label="",style="dashed", color="green", weight=3];
339[label="Succ wu210",fontsize=16,color="green",shape="box"];340[label="primMinusNat (Succ wu2100) wu2300",fontsize=16,color="burlywood",shape="box"];532[label="wu2300/Succ wu23000",fontsize=10,color="white",style="solid",shape="box"];340 -> 532[label="",style="solid", color="burlywood", weight=9];
532 -> 352[label="",style="solid", color="burlywood", weight=3];
533[label="wu2300/Zero",fontsize=10,color="white",style="solid",shape="box"];340 -> 533[label="",style="solid", color="burlywood", weight=9];
533 -> 353[label="",style="solid", color="burlywood", weight=3];
341[label="primMinusNat Zero wu2300",fontsize=16,color="burlywood",shape="box"];534[label="wu2300/Succ wu23000",fontsize=10,color="white",style="solid",shape="box"];341 -> 534[label="",style="solid", color="burlywood", weight=9];
534 -> 354[label="",style="solid", color="burlywood", weight=3];
535[label="wu2300/Zero",fontsize=10,color="white",style="solid",shape="box"];341 -> 535[label="",style="solid", color="burlywood", weight=9];
535 -> 355[label="",style="solid", color="burlywood", weight=3];
342[label="wu2200",fontsize=16,color="green",shape="box"];343[label="wu2300",fontsize=16,color="green",shape="box"];344[label="Succ wu2300",fontsize=16,color="green",shape="box"];345[label="Zero",fontsize=16,color="green",shape="box"];346 -> 322[label="",style="dashed", color="red", weight=0];
346[label="primPlusNat wu210 wu2200",fontsize=16,color="magenta"];347[label="primPlusNat (Succ wu2100) wu2200",fontsize=16,color="burlywood",shape="box"];537[label="wu2200/Succ wu22000",fontsize=10,color="white",style="solid",shape="box"];347 -> 537[label="",style="solid", color="burlywood", weight=9];
537 -> 356[label="",style="solid", color="burlywood", weight=3];
538[label="wu2200/Zero",fontsize=10,color="white",style="solid",shape="box"];347 -> 538[label="",style="solid", color="burlywood", weight=9];
538 -> 357[label="",style="solid", color="burlywood", weight=3];
348[label="primPlusNat Zero wu2200",fontsize=16,color="burlywood",shape="box"];539[label="wu2200/Succ wu22000",fontsize=10,color="white",style="solid",shape="box"];348 -> 539[label="",style="solid", color="burlywood", weight=9];
539 -> 358[label="",style="solid", color="burlywood", weight=3];
540[label="wu2200/Zero",fontsize=10,color="white",style="solid",shape="box"];348 -> 540[label="",style="solid", color="burlywood", weight=9];
540 -> 359[label="",style="solid", color="burlywood", weight=3];
349 -> 322[label="",style="dashed", color="red", weight=0];
349[label="primPlusNat wu280 wu2900",fontsize=16,color="magenta"];349 -> 360[label="",style="dashed", color="magenta", weight=3];
349 -> 361[label="",style="dashed", color="magenta", weight=3];
350 -> 322[label="",style="dashed", color="red", weight=0];
350[label="primPlusNat wu280 wu2900",fontsize=16,color="magenta"];350 -> 362[label="",style="dashed", color="magenta", weight=3];
350 -> 363[label="",style="dashed", color="magenta", weight=3];
351 -> 322[label="",style="dashed", color="red", weight=0];
351[label="primPlusNat wu210 wu2300",fontsize=16,color="magenta"];351 -> 364[label="",style="dashed", color="magenta", weight=3];
352[label="primMinusNat (Succ wu2100) (Succ wu23000)",fontsize=16,color="black",shape="box"];352 -> 365[label="",style="solid", color="black", weight=3];
353[label="primMinusNat (Succ wu2100) Zero",fontsize=16,color="black",shape="box"];353 -> 366[label="",style="solid", color="black", weight=3];
354[label="primMinusNat Zero (Succ wu23000)",fontsize=16,color="black",shape="box"];354 -> 367[label="",style="solid", color="black", weight=3];
355[label="primMinusNat Zero Zero",fontsize=16,color="black",shape="box"];355 -> 368[label="",style="solid", color="black", weight=3];
356[label="primPlusNat (Succ wu2100) (Succ wu22000)",fontsize=16,color="black",shape="box"];356 -> 369[label="",style="solid", color="black", weight=3];
357[label="primPlusNat (Succ wu2100) Zero",fontsize=16,color="black",shape="box"];357 -> 370[label="",style="solid", color="black", weight=3];
358[label="primPlusNat Zero (Succ wu22000)",fontsize=16,color="black",shape="box"];358 -> 371[label="",style="solid", color="black", weight=3];
359[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];359 -> 372[label="",style="solid", color="black", weight=3];
360[label="wu2900",fontsize=16,color="green",shape="box"];361[label="wu280",fontsize=16,color="green",shape="box"];362[label="wu2900",fontsize=16,color="green",shape="box"];363[label="wu280",fontsize=16,color="green",shape="box"];364[label="wu2300",fontsize=16,color="green",shape="box"];365 -> 310[label="",style="dashed", color="red", weight=0];
365[label="primMinusNat wu2100 wu23000",fontsize=16,color="magenta"];365 -> 373[label="",style="dashed", color="magenta", weight=3];
365 -> 374[label="",style="dashed", color="magenta", weight=3];
366[label="Pos (Succ wu2100)",fontsize=16,color="green",shape="box"];367[label="Neg (Succ wu23000)",fontsize=16,color="green",shape="box"];368[label="Pos Zero",fontsize=16,color="green",shape="box"];369[label="Succ (Succ (primPlusNat wu2100 wu22000))",fontsize=16,color="green",shape="box"];369 -> 375[label="",style="dashed", color="green", weight=3];
370[label="Succ wu2100",fontsize=16,color="green",shape="box"];371[label="Succ wu22000",fontsize=16,color="green",shape="box"];372[label="Zero",fontsize=16,color="green",shape="box"];373[label="wu23000",fontsize=16,color="green",shape="box"];374[label="wu2100",fontsize=16,color="green",shape="box"];375 -> 322[label="",style="dashed", color="red", weight=0];
375[label="primPlusNat wu2100 wu22000",fontsize=16,color="magenta"];375 -> 376[label="",style="dashed", color="magenta", weight=3];
375 -> 377[label="",style="dashed", color="magenta", weight=3];
376[label="wu22000",fontsize=16,color="green",shape="box"];377[label="wu2100",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(wu2100), Succ(wu23000)) → new_primMinusNat(wu2100, wu23000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primMinusNat(Succ(wu2100), Succ(wu23000)) → new_primMinusNat(wu2100, wu23000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(wu2100), Succ(wu22000)) → new_primPlusNat(wu2100, wu22000)

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(wu2100), Succ(wu22000)) → new_primPlusNat(wu2100, wu22000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primPlusInt(Succ(wu210), Succ(wu2200), wu23) → new_primPlusInt(wu210, wu2200, wu23)

From the DPs we obtained the following set of size-change graphs:

new_primPlusInt(Succ(wu210), Succ(wu2200), wu23) → new_primPlusInt(wu210, wu2200, wu23)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ Rewriting

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_map(wu6, wu7, wu8, ba, bb, bc) → new_map(wu6, wu7, new_ps(wu6, wu7, wu8, bb, bc), ba, bb, bc)

The TRS R consists of the following rules:

new_fromEnum6(wu15, ty_Char) → new_fromEnum7(wu15)
new_primPlusInt0(Zero, Neg(Zero), Neg(wu230)) → new_primMinusNat1(wu230)
new_fromEnum6(wu15, ty_Double) → new_fromEnum4(wu15)
new_fromEnum6(wu15, app(ty_Ratio, bf)) → new_fromEnum(wu15, bf)
new_primPlusNat2(wu210, Succ(wu2300)) → Succ(Succ(new_primPlusNat1(wu210, wu2300)))
new_primPlusInt1(Succ(wu210), Zero, Pos(wu230)) → Pos(new_primPlusNat2(wu210, wu230))
new_primPlusNat2(wu210, Zero) → Succ(wu210)
new_primPlusNat0(Succ(wu210), Zero, wu230) → new_primPlusNat2(wu210, wu230)
new_primPlusNat0(Zero, Succ(wu2200), wu230) → new_primPlusNat2(wu2200, wu230)
new_primPlusInt1(Zero, Zero, Pos(wu230)) → Pos(new_primPlusNat3(wu230))
new_fromEnum5(wu15, ty_Bool) → new_fromEnum3(wu15)
new_primPlusInt3(Pos(wu140), wu15, wu16, be) → new_primPlusInt0(wu140, new_fromEnum5(wu15, be), wu16)
new_primMinusNat2(Succ(wu2300), wu2200) → new_primMinusNat3(wu2300, wu2200)
new_fromEnum10(wu6, ty_Float) → new_fromEnum0(wu6)
new_primPlusInt1(Zero, Zero, Neg(wu230)) → new_primMinusNat1(wu230)
new_primPlusNat1(Succ(wu2100), Succ(wu22000)) → Succ(Succ(new_primPlusNat1(wu2100, wu22000)))
new_primMinusNat0(wu210, Zero) → Pos(Succ(wu210))
new_primPlusInt2(Succ(wu280), Pos(Zero), Pos(Zero)) → new_primMinusNat2(Zero, wu280)
new_primPlusInt2(Succ(wu280), Pos(Zero), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), wu280)
new_fromEnum10(wu6, ty_Int) → new_fromEnum8(wu6)
new_fromEnum10(wu6, ty_Double) → new_fromEnum4(wu6)
new_fromEnum6(wu15, ty_Integer) → new_fromEnum1(wu15)
new_primMinusNat2(Zero, wu2200) → Neg(Succ(wu2200))
new_fromEnum8(wu6) → error([])
new_fromEnum2(@0) → Pos(Zero)
new_primPlusInt1(Succ(wu210), Zero, Neg(wu230)) → new_primMinusNat0(wu210, wu230)
new_fromEnum10(wu6, ty_Integer) → new_fromEnum1(wu6)
new_fromEnum10(wu6, ty_@0) → new_fromEnum2(wu6)
new_primPlusNat1(Zero, Zero) → Zero
new_fromEnum6(wu15, ty_Float) → new_fromEnum0(wu15)
new_primPlusInt1(Zero, Succ(wu2200), Pos(wu230)) → new_primMinusNat2(wu230, wu2200)
new_fromEnum5(wu15, ty_Int) → new_fromEnum8(wu15)
new_primMinusNat3(Zero, Succ(wu23000)) → Neg(Succ(wu23000))
new_fromEnum6(wu15, ty_@0) → new_fromEnum2(wu15)
new_primPlusInt0(Succ(wu210), Neg(Succ(wu2200)), Neg(wu230)) → new_primMinusNat0(Succ(new_primPlusNat1(wu210, wu2200)), wu230)
new_primPlusInt0(Zero, Neg(Succ(wu2200)), Neg(wu230)) → new_primMinusNat0(wu2200, wu230)
new_primPlusNat3(Zero) → Zero
new_fromEnum3(wu6) → error([])
new_fromEnum5(wu15, ty_Float) → new_fromEnum0(wu15)
new_primPlusInt1(Zero, Succ(wu2200), Neg(wu230)) → Neg(new_primPlusNat2(wu2200, wu230))
new_fromEnum5(wu15, ty_Ordering) → new_fromEnum9(wu15)
new_primPlusInt0(Succ(wu210), Neg(Zero), Neg(wu230)) → new_primMinusNat0(wu210, wu230)
new_fromEnum5(wu15, ty_Double) → new_fromEnum4(wu15)
new_primPlusInt0(wu21, Neg(wu220), Pos(wu230)) → Pos(new_primPlusNat0(wu21, wu220, wu230))
new_primPlusInt2(Zero, Pos(Succ(wu2900)), Pos(Zero)) → new_primMinusNat2(Zero, wu2900)
new_fromEnum(wu6, bd) → error([])
new_primMinusNat0(wu210, Succ(wu2300)) → new_primMinusNat3(wu210, wu2300)
new_primPlusInt2(Zero, Pos(Zero), Pos(Succ(wu3000))) → new_primMinusNat0(wu3000, Zero)
new_fromEnum10(wu6, ty_Bool) → new_fromEnum3(wu6)
new_fromEnum0(wu6) → error([])
new_fromEnum10(wu6, ty_Ordering) → new_fromEnum9(wu6)
new_primMinusNat3(Succ(wu2100), Zero) → Pos(Succ(wu2100))
new_primPlusNat3(Succ(wu2300)) → Succ(wu2300)
new_primMinusNat1(Zero) → Pos(Zero)
new_primPlusInt3(Neg(wu140), wu15, wu16, be) → new_primPlusInt2(wu140, new_fromEnum6(wu15, be), wu16)
new_primPlusInt2(wu28, Pos(wu290), Neg(wu300)) → Neg(new_primPlusNat0(wu28, wu290, wu300))
new_primPlusInt0(wu21, Pos(wu220), wu23) → new_primPlusInt1(wu21, wu220, wu23)
new_fromEnum5(wu15, ty_Integer) → new_fromEnum1(wu15)
new_primPlusInt2(Succ(wu280), Pos(Succ(wu2900)), Pos(Zero)) → new_primMinusNat2(Zero, Succ(new_primPlusNat1(wu280, wu2900)))
new_fromEnum4(wu6) → error([])
new_primMinusNat3(Zero, Zero) → Pos(Zero)
new_fromEnum9(wu6) → error([])
new_fromEnum6(wu15, ty_Int) → new_fromEnum8(wu15)
new_fromEnum1(wu6) → error([])
new_primPlusInt2(Zero, Pos(Succ(wu2900)), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), wu2900)
new_primPlusInt2(wu28, Neg(wu290), wu30) → new_primPlusInt1(wu290, wu28, wu30)
new_fromEnum10(wu6, app(ty_Ratio, bd)) → new_fromEnum(wu6, bd)
new_primPlusNat1(Succ(wu2100), Zero) → Succ(wu2100)
new_primPlusNat1(Zero, Succ(wu22000)) → Succ(wu22000)
new_fromEnum7(wu6) → error([])
new_primMinusNat1(Succ(wu2300)) → Neg(Succ(wu2300))
new_primPlusInt2(Zero, Pos(Zero), Pos(Zero)) → new_primMinusNat1(Zero)
new_fromEnum6(wu15, ty_Bool) → new_fromEnum3(wu15)
new_primMinusNat3(Succ(wu2100), Succ(wu23000)) → new_primMinusNat3(wu2100, wu23000)
new_fromEnum5(wu15, ty_@0) → new_fromEnum2(wu15)
new_ps(wu6, wu7, wu8, bb, bc) → new_primPlusInt3(new_fromEnum10(wu6, bb), wu7, wu8, bc)
new_primPlusInt2(Succ(wu280), Pos(Succ(wu2900)), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), Succ(new_primPlusNat1(wu280, wu2900)))
new_fromEnum10(wu6, ty_Char) → new_fromEnum7(wu6)
new_primPlusNat0(Succ(wu210), Succ(wu2200), wu230) → new_primPlusNat2(Succ(new_primPlusNat1(wu210, wu2200)), wu230)
new_fromEnum6(wu15, ty_Ordering) → new_fromEnum9(wu15)
new_fromEnum5(wu15, ty_Char) → new_fromEnum7(wu15)
new_primPlusNat0(Zero, Zero, wu230) → new_primPlusNat3(wu230)
new_primPlusInt1(Succ(wu210), Succ(wu2200), wu23) → new_primPlusInt1(wu210, wu2200, wu23)
new_fromEnum5(wu15, app(ty_Ratio, bf)) → new_fromEnum(wu15, bf)

The set Q consists of the following terms:

new_fromEnum6(x0, ty_Ordering)
new_fromEnum8(x0)
new_primMinusNat2(Succ(x0), x1)
new_fromEnum7(x0)
new_primPlusInt0(Succ(x0), Neg(Succ(x1)), Neg(x2))
new_primPlusInt2(Succ(x0), Pos(Zero), Pos(Zero))
new_fromEnum5(x0, ty_Double)
new_primPlusInt1(Succ(x0), Succ(x1), x2)
new_fromEnum5(x0, ty_Ordering)
new_primPlusNat3(Succ(x0))
new_fromEnum6(x0, ty_@0)
new_ps(x0, x1, x2, x3, x4)
new_fromEnum10(x0, ty_Char)
new_fromEnum9(x0)
new_primPlusInt0(Zero, Neg(Succ(x0)), Neg(x1))
new_primPlusInt0(Zero, Neg(Zero), Neg(x0))
new_fromEnum5(x0, ty_Int)
new_primPlusNat1(Zero, Succ(x0))
new_fromEnum10(x0, ty_@0)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primPlusNat2(x0, Zero)
new_primPlusInt1(Succ(x0), Zero, Neg(x1))
new_fromEnum(x0, x1)
new_fromEnum10(x0, ty_Integer)
new_primPlusInt2(Zero, Pos(Succ(x0)), Pos(Zero))
new_primPlusInt1(Zero, Zero, Neg(x0))
new_primPlusNat1(Succ(x0), Zero)
new_primPlusInt2(x0, Neg(x1), x2)
new_primPlusInt0(x0, Pos(x1), x2)
new_fromEnum3(x0)
new_fromEnum6(x0, app(ty_Ratio, x1))
new_primPlusInt2(Succ(x0), Pos(Zero), Pos(Succ(x1)))
new_fromEnum5(x0, ty_@0)
new_primPlusNat0(Succ(x0), Succ(x1), x2)
new_primPlusInt0(Succ(x0), Neg(Zero), Neg(x1))
new_primMinusNat1(Succ(x0))
new_primPlusNat1(Zero, Zero)
new_primPlusNat0(Zero, Zero, x0)
new_fromEnum4(x0)
new_fromEnum6(x0, ty_Bool)
new_fromEnum6(x0, ty_Float)
new_primPlusInt2(Succ(x0), Pos(Succ(x1)), Pos(Zero))
new_fromEnum10(x0, ty_Double)
new_primPlusInt1(Zero, Succ(x0), Neg(x1))
new_primMinusNat3(Zero, Zero)
new_fromEnum5(x0, ty_Integer)
new_fromEnum6(x0, ty_Integer)
new_primPlusInt2(Zero, Pos(Zero), Pos(Succ(x0)))
new_fromEnum1(x0)
new_primPlusInt1(Zero, Zero, Pos(x0))
new_fromEnum10(x0, ty_Int)
new_fromEnum5(x0, ty_Char)
new_primPlusInt2(Succ(x0), Pos(Succ(x1)), Pos(Succ(x2)))
new_fromEnum6(x0, ty_Double)
new_primMinusNat3(Zero, Succ(x0))
new_primMinusNat1(Zero)
new_primPlusInt0(x0, Neg(x1), Pos(x2))
new_primMinusNat3(Succ(x0), Succ(x1))
new_fromEnum5(x0, app(ty_Ratio, x1))
new_fromEnum2(@0)
new_primPlusInt2(x0, Pos(x1), Neg(x2))
new_fromEnum10(x0, ty_Float)
new_fromEnum0(x0)
new_primMinusNat0(x0, Zero)
new_primPlusNat3(Zero)
new_primMinusNat2(Zero, x0)
new_primPlusNat0(Zero, Succ(x0), x1)
new_fromEnum5(x0, ty_Float)
new_fromEnum10(x0, ty_Ordering)
new_primPlusInt1(Succ(x0), Zero, Pos(x1))
new_primPlusInt1(Zero, Succ(x0), Pos(x1))
new_primMinusNat3(Succ(x0), Zero)
new_primPlusNat2(x0, Succ(x1))
new_primPlusInt2(Zero, Pos(Zero), Pos(Zero))
new_fromEnum10(x0, app(ty_Ratio, x1))
new_primPlusInt3(Pos(x0), x1, x2, x3)
new_fromEnum6(x0, ty_Char)
new_primPlusInt2(Zero, Pos(Succ(x0)), Pos(Succ(x1)))
new_primPlusNat0(Succ(x0), Zero, x1)
new_primMinusNat0(x0, Succ(x1))
new_primPlusInt3(Neg(x0), x1, x2, x3)
new_fromEnum6(x0, ty_Int)
new_fromEnum5(x0, ty_Bool)
new_fromEnum10(x0, ty_Bool)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_map(wu6, wu7, wu8, ba, bb, bc) → new_map(wu6, wu7, new_ps(wu6, wu7, wu8, bb, bc), ba, bb, bc) at position [2] we obtained the following new rules:

new_map(wu6, wu7, wu8, ba, bb, bc) → new_map(wu6, wu7, new_primPlusInt3(new_fromEnum10(wu6, bb), wu7, wu8, bc), ba, bb, bc)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ Rewriting

                      ↳ QDP

                        ↳ UsableRulesProof

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_map(wu6, wu7, wu8, ba, bb, bc) → new_map(wu6, wu7, new_primPlusInt3(new_fromEnum10(wu6, bb), wu7, wu8, bc), ba, bb, bc)

The TRS R consists of the following rules:

new_fromEnum6(wu15, ty_Char) → new_fromEnum7(wu15)
new_primPlusInt0(Zero, Neg(Zero), Neg(wu230)) → new_primMinusNat1(wu230)
new_fromEnum6(wu15, ty_Double) → new_fromEnum4(wu15)
new_fromEnum6(wu15, app(ty_Ratio, bf)) → new_fromEnum(wu15, bf)
new_primPlusNat2(wu210, Succ(wu2300)) → Succ(Succ(new_primPlusNat1(wu210, wu2300)))
new_primPlusInt1(Succ(wu210), Zero, Pos(wu230)) → Pos(new_primPlusNat2(wu210, wu230))
new_primPlusNat2(wu210, Zero) → Succ(wu210)
new_primPlusNat0(Succ(wu210), Zero, wu230) → new_primPlusNat2(wu210, wu230)
new_primPlusNat0(Zero, Succ(wu2200), wu230) → new_primPlusNat2(wu2200, wu230)
new_primPlusInt1(Zero, Zero, Pos(wu230)) → Pos(new_primPlusNat3(wu230))
new_fromEnum5(wu15, ty_Bool) → new_fromEnum3(wu15)
new_primPlusInt3(Pos(wu140), wu15, wu16, be) → new_primPlusInt0(wu140, new_fromEnum5(wu15, be), wu16)
new_primMinusNat2(Succ(wu2300), wu2200) → new_primMinusNat3(wu2300, wu2200)
new_fromEnum10(wu6, ty_Float) → new_fromEnum0(wu6)
new_primPlusInt1(Zero, Zero, Neg(wu230)) → new_primMinusNat1(wu230)
new_primPlusNat1(Succ(wu2100), Succ(wu22000)) → Succ(Succ(new_primPlusNat1(wu2100, wu22000)))
new_primMinusNat0(wu210, Zero) → Pos(Succ(wu210))
new_primPlusInt2(Succ(wu280), Pos(Zero), Pos(Zero)) → new_primMinusNat2(Zero, wu280)
new_primPlusInt2(Succ(wu280), Pos(Zero), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), wu280)
new_fromEnum10(wu6, ty_Int) → new_fromEnum8(wu6)
new_fromEnum10(wu6, ty_Double) → new_fromEnum4(wu6)
new_fromEnum6(wu15, ty_Integer) → new_fromEnum1(wu15)
new_primMinusNat2(Zero, wu2200) → Neg(Succ(wu2200))
new_fromEnum8(wu6) → error([])
new_fromEnum2(@0) → Pos(Zero)
new_primPlusInt1(Succ(wu210), Zero, Neg(wu230)) → new_primMinusNat0(wu210, wu230)
new_fromEnum10(wu6, ty_Integer) → new_fromEnum1(wu6)
new_fromEnum10(wu6, ty_@0) → new_fromEnum2(wu6)
new_primPlusNat1(Zero, Zero) → Zero
new_fromEnum6(wu15, ty_Float) → new_fromEnum0(wu15)
new_primPlusInt1(Zero, Succ(wu2200), Pos(wu230)) → new_primMinusNat2(wu230, wu2200)
new_fromEnum5(wu15, ty_Int) → new_fromEnum8(wu15)
new_primMinusNat3(Zero, Succ(wu23000)) → Neg(Succ(wu23000))
new_fromEnum6(wu15, ty_@0) → new_fromEnum2(wu15)
new_primPlusInt0(Succ(wu210), Neg(Succ(wu2200)), Neg(wu230)) → new_primMinusNat0(Succ(new_primPlusNat1(wu210, wu2200)), wu230)
new_primPlusInt0(Zero, Neg(Succ(wu2200)), Neg(wu230)) → new_primMinusNat0(wu2200, wu230)
new_primPlusNat3(Zero) → Zero
new_fromEnum3(wu6) → error([])
new_fromEnum5(wu15, ty_Float) → new_fromEnum0(wu15)
new_primPlusInt1(Zero, Succ(wu2200), Neg(wu230)) → Neg(new_primPlusNat2(wu2200, wu230))
new_fromEnum5(wu15, ty_Ordering) → new_fromEnum9(wu15)
new_primPlusInt0(Succ(wu210), Neg(Zero), Neg(wu230)) → new_primMinusNat0(wu210, wu230)
new_fromEnum5(wu15, ty_Double) → new_fromEnum4(wu15)
new_primPlusInt0(wu21, Neg(wu220), Pos(wu230)) → Pos(new_primPlusNat0(wu21, wu220, wu230))
new_primPlusInt2(Zero, Pos(Succ(wu2900)), Pos(Zero)) → new_primMinusNat2(Zero, wu2900)
new_fromEnum(wu6, bd) → error([])
new_primMinusNat0(wu210, Succ(wu2300)) → new_primMinusNat3(wu210, wu2300)
new_primPlusInt2(Zero, Pos(Zero), Pos(Succ(wu3000))) → new_primMinusNat0(wu3000, Zero)
new_fromEnum10(wu6, ty_Bool) → new_fromEnum3(wu6)
new_fromEnum0(wu6) → error([])
new_fromEnum10(wu6, ty_Ordering) → new_fromEnum9(wu6)
new_primMinusNat3(Succ(wu2100), Zero) → Pos(Succ(wu2100))
new_primPlusNat3(Succ(wu2300)) → Succ(wu2300)
new_primMinusNat1(Zero) → Pos(Zero)
new_primPlusInt3(Neg(wu140), wu15, wu16, be) → new_primPlusInt2(wu140, new_fromEnum6(wu15, be), wu16)
new_primPlusInt2(wu28, Pos(wu290), Neg(wu300)) → Neg(new_primPlusNat0(wu28, wu290, wu300))
new_primPlusInt0(wu21, Pos(wu220), wu23) → new_primPlusInt1(wu21, wu220, wu23)
new_fromEnum5(wu15, ty_Integer) → new_fromEnum1(wu15)
new_primPlusInt2(Succ(wu280), Pos(Succ(wu2900)), Pos(Zero)) → new_primMinusNat2(Zero, Succ(new_primPlusNat1(wu280, wu2900)))
new_fromEnum4(wu6) → error([])
new_primMinusNat3(Zero, Zero) → Pos(Zero)
new_fromEnum9(wu6) → error([])
new_fromEnum6(wu15, ty_Int) → new_fromEnum8(wu15)
new_fromEnum1(wu6) → error([])
new_primPlusInt2(Zero, Pos(Succ(wu2900)), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), wu2900)
new_primPlusInt2(wu28, Neg(wu290), wu30) → new_primPlusInt1(wu290, wu28, wu30)
new_fromEnum10(wu6, app(ty_Ratio, bd)) → new_fromEnum(wu6, bd)
new_primPlusNat1(Succ(wu2100), Zero) → Succ(wu2100)
new_primPlusNat1(Zero, Succ(wu22000)) → Succ(wu22000)
new_fromEnum7(wu6) → error([])
new_primMinusNat1(Succ(wu2300)) → Neg(Succ(wu2300))
new_primPlusInt2(Zero, Pos(Zero), Pos(Zero)) → new_primMinusNat1(Zero)
new_fromEnum6(wu15, ty_Bool) → new_fromEnum3(wu15)
new_primMinusNat3(Succ(wu2100), Succ(wu23000)) → new_primMinusNat3(wu2100, wu23000)
new_fromEnum5(wu15, ty_@0) → new_fromEnum2(wu15)
new_ps(wu6, wu7, wu8, bb, bc) → new_primPlusInt3(new_fromEnum10(wu6, bb), wu7, wu8, bc)
new_primPlusInt2(Succ(wu280), Pos(Succ(wu2900)), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), Succ(new_primPlusNat1(wu280, wu2900)))
new_fromEnum10(wu6, ty_Char) → new_fromEnum7(wu6)
new_primPlusNat0(Succ(wu210), Succ(wu2200), wu230) → new_primPlusNat2(Succ(new_primPlusNat1(wu210, wu2200)), wu230)
new_fromEnum6(wu15, ty_Ordering) → new_fromEnum9(wu15)
new_fromEnum5(wu15, ty_Char) → new_fromEnum7(wu15)
new_primPlusNat0(Zero, Zero, wu230) → new_primPlusNat3(wu230)
new_primPlusInt1(Succ(wu210), Succ(wu2200), wu23) → new_primPlusInt1(wu210, wu2200, wu23)
new_fromEnum5(wu15, app(ty_Ratio, bf)) → new_fromEnum(wu15, bf)

The set Q consists of the following terms:

new_fromEnum6(x0, ty_Ordering)
new_fromEnum8(x0)
new_primMinusNat2(Succ(x0), x1)
new_fromEnum7(x0)
new_primPlusInt0(Succ(x0), Neg(Succ(x1)), Neg(x2))
new_primPlusInt2(Succ(x0), Pos(Zero), Pos(Zero))
new_fromEnum5(x0, ty_Double)
new_primPlusInt1(Succ(x0), Succ(x1), x2)
new_fromEnum5(x0, ty_Ordering)
new_primPlusNat3(Succ(x0))
new_fromEnum6(x0, ty_@0)
new_ps(x0, x1, x2, x3, x4)
new_fromEnum10(x0, ty_Char)
new_fromEnum9(x0)
new_primPlusInt0(Zero, Neg(Succ(x0)), Neg(x1))
new_primPlusInt0(Zero, Neg(Zero), Neg(x0))
new_fromEnum5(x0, ty_Int)
new_primPlusNat1(Zero, Succ(x0))
new_fromEnum10(x0, ty_@0)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primPlusNat2(x0, Zero)
new_primPlusInt1(Succ(x0), Zero, Neg(x1))
new_fromEnum(x0, x1)
new_fromEnum10(x0, ty_Integer)
new_primPlusInt2(Zero, Pos(Succ(x0)), Pos(Zero))
new_primPlusInt1(Zero, Zero, Neg(x0))
new_primPlusNat1(Succ(x0), Zero)
new_primPlusInt2(x0, Neg(x1), x2)
new_primPlusInt0(x0, Pos(x1), x2)
new_fromEnum3(x0)
new_fromEnum6(x0, app(ty_Ratio, x1))
new_primPlusInt2(Succ(x0), Pos(Zero), Pos(Succ(x1)))
new_fromEnum5(x0, ty_@0)
new_primPlusNat0(Succ(x0), Succ(x1), x2)
new_primPlusInt0(Succ(x0), Neg(Zero), Neg(x1))
new_primMinusNat1(Succ(x0))
new_primPlusNat1(Zero, Zero)
new_primPlusNat0(Zero, Zero, x0)
new_fromEnum4(x0)
new_fromEnum6(x0, ty_Bool)
new_fromEnum6(x0, ty_Float)
new_primPlusInt2(Succ(x0), Pos(Succ(x1)), Pos(Zero))
new_fromEnum10(x0, ty_Double)
new_primPlusInt1(Zero, Succ(x0), Neg(x1))
new_primMinusNat3(Zero, Zero)
new_fromEnum5(x0, ty_Integer)
new_fromEnum6(x0, ty_Integer)
new_primPlusInt2(Zero, Pos(Zero), Pos(Succ(x0)))
new_fromEnum1(x0)
new_primPlusInt1(Zero, Zero, Pos(x0))
new_fromEnum10(x0, ty_Int)
new_fromEnum5(x0, ty_Char)
new_primPlusInt2(Succ(x0), Pos(Succ(x1)), Pos(Succ(x2)))
new_fromEnum6(x0, ty_Double)
new_primMinusNat3(Zero, Succ(x0))
new_primMinusNat1(Zero)
new_primPlusInt0(x0, Neg(x1), Pos(x2))
new_primMinusNat3(Succ(x0), Succ(x1))
new_fromEnum5(x0, app(ty_Ratio, x1))
new_fromEnum2(@0)
new_primPlusInt2(x0, Pos(x1), Neg(x2))
new_fromEnum10(x0, ty_Float)
new_fromEnum0(x0)
new_primMinusNat0(x0, Zero)
new_primPlusNat3(Zero)
new_primMinusNat2(Zero, x0)
new_primPlusNat0(Zero, Succ(x0), x1)
new_fromEnum5(x0, ty_Float)
new_fromEnum10(x0, ty_Ordering)
new_primPlusInt1(Succ(x0), Zero, Pos(x1))
new_primPlusInt1(Zero, Succ(x0), Pos(x1))
new_primMinusNat3(Succ(x0), Zero)
new_primPlusNat2(x0, Succ(x1))
new_primPlusInt2(Zero, Pos(Zero), Pos(Zero))
new_fromEnum10(x0, app(ty_Ratio, x1))
new_primPlusInt3(Pos(x0), x1, x2, x3)
new_fromEnum6(x0, ty_Char)
new_primPlusInt2(Zero, Pos(Succ(x0)), Pos(Succ(x1)))
new_primPlusNat0(Succ(x0), Zero, x1)
new_primMinusNat0(x0, Succ(x1))
new_primPlusInt3(Neg(x0), x1, x2, x3)
new_fromEnum6(x0, ty_Int)
new_fromEnum5(x0, ty_Bool)
new_fromEnum10(x0, ty_Bool)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ Rewriting

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_map(wu6, wu7, wu8, ba, bb, bc) → new_map(wu6, wu7, new_primPlusInt3(new_fromEnum10(wu6, bb), wu7, wu8, bc), ba, bb, bc)

The TRS R consists of the following rules:

new_fromEnum10(wu6, ty_Float) → new_fromEnum0(wu6)
new_fromEnum10(wu6, ty_Int) → new_fromEnum8(wu6)
new_fromEnum10(wu6, ty_Double) → new_fromEnum4(wu6)
new_fromEnum10(wu6, ty_Integer) → new_fromEnum1(wu6)
new_fromEnum10(wu6, ty_@0) → new_fromEnum2(wu6)
new_fromEnum10(wu6, ty_Bool) → new_fromEnum3(wu6)
new_fromEnum10(wu6, ty_Ordering) → new_fromEnum9(wu6)
new_fromEnum10(wu6, app(ty_Ratio, bd)) → new_fromEnum(wu6, bd)
new_fromEnum10(wu6, ty_Char) → new_fromEnum7(wu6)
new_primPlusInt3(Pos(wu140), wu15, wu16, be) → new_primPlusInt0(wu140, new_fromEnum5(wu15, be), wu16)
new_primPlusInt3(Neg(wu140), wu15, wu16, be) → new_primPlusInt2(wu140, new_fromEnum6(wu15, be), wu16)
new_fromEnum6(wu15, ty_Char) → new_fromEnum7(wu15)
new_fromEnum6(wu15, ty_Double) → new_fromEnum4(wu15)
new_fromEnum6(wu15, app(ty_Ratio, bf)) → new_fromEnum(wu15, bf)
new_fromEnum6(wu15, ty_Integer) → new_fromEnum1(wu15)
new_fromEnum6(wu15, ty_Float) → new_fromEnum0(wu15)
new_fromEnum6(wu15, ty_@0) → new_fromEnum2(wu15)
new_fromEnum6(wu15, ty_Int) → new_fromEnum8(wu15)
new_fromEnum6(wu15, ty_Bool) → new_fromEnum3(wu15)
new_fromEnum6(wu15, ty_Ordering) → new_fromEnum9(wu15)
new_primPlusInt2(Succ(wu280), Pos(Zero), Pos(Zero)) → new_primMinusNat2(Zero, wu280)
new_primPlusInt2(Succ(wu280), Pos(Zero), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), wu280)
new_primPlusInt2(Zero, Pos(Succ(wu2900)), Pos(Zero)) → new_primMinusNat2(Zero, wu2900)
new_primPlusInt2(Zero, Pos(Zero), Pos(Succ(wu3000))) → new_primMinusNat0(wu3000, Zero)
new_primPlusInt2(wu28, Pos(wu290), Neg(wu300)) → Neg(new_primPlusNat0(wu28, wu290, wu300))
new_primPlusInt2(Succ(wu280), Pos(Succ(wu2900)), Pos(Zero)) → new_primMinusNat2(Zero, Succ(new_primPlusNat1(wu280, wu2900)))
new_primPlusInt2(Zero, Pos(Succ(wu2900)), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), wu2900)
new_primPlusInt2(wu28, Neg(wu290), wu30) → new_primPlusInt1(wu290, wu28, wu30)
new_primPlusInt2(Zero, Pos(Zero), Pos(Zero)) → new_primMinusNat1(Zero)
new_primPlusInt2(Succ(wu280), Pos(Succ(wu2900)), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), Succ(new_primPlusNat1(wu280, wu2900)))
new_primPlusNat1(Succ(wu2100), Succ(wu22000)) → Succ(Succ(new_primPlusNat1(wu2100, wu22000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Succ(wu2100), Zero) → Succ(wu2100)
new_primPlusNat1(Zero, Succ(wu22000)) → Succ(wu22000)
new_primMinusNat2(Succ(wu2300), wu2200) → new_primMinusNat3(wu2300, wu2200)
new_primMinusNat3(Zero, Succ(wu23000)) → Neg(Succ(wu23000))
new_primMinusNat3(Succ(wu2100), Zero) → Pos(Succ(wu2100))
new_primMinusNat3(Zero, Zero) → Pos(Zero)
new_primMinusNat3(Succ(wu2100), Succ(wu23000)) → new_primMinusNat3(wu2100, wu23000)
new_primMinusNat1(Zero) → Pos(Zero)
new_primPlusInt1(Succ(wu210), Zero, Pos(wu230)) → Pos(new_primPlusNat2(wu210, wu230))
new_primPlusInt1(Zero, Zero, Pos(wu230)) → Pos(new_primPlusNat3(wu230))
new_primPlusInt1(Zero, Zero, Neg(wu230)) → new_primMinusNat1(wu230)
new_primPlusInt1(Succ(wu210), Zero, Neg(wu230)) → new_primMinusNat0(wu210, wu230)
new_primPlusInt1(Zero, Succ(wu2200), Pos(wu230)) → new_primMinusNat2(wu230, wu2200)
new_primPlusInt1(Zero, Succ(wu2200), Neg(wu230)) → Neg(new_primPlusNat2(wu2200, wu230))
new_primPlusInt1(Succ(wu210), Succ(wu2200), wu23) → new_primPlusInt1(wu210, wu2200, wu23)
new_primPlusNat2(wu210, Succ(wu2300)) → Succ(Succ(new_primPlusNat1(wu210, wu2300)))
new_primPlusNat2(wu210, Zero) → Succ(wu210)
new_primMinusNat2(Zero, wu2200) → Neg(Succ(wu2200))
new_primMinusNat0(wu210, Zero) → Pos(Succ(wu210))
new_primMinusNat0(wu210, Succ(wu2300)) → new_primMinusNat3(wu210, wu2300)
new_primMinusNat1(Succ(wu2300)) → Neg(Succ(wu2300))
new_primPlusNat3(Zero) → Zero
new_primPlusNat3(Succ(wu2300)) → Succ(wu2300)
new_primPlusNat0(Succ(wu210), Zero, wu230) → new_primPlusNat2(wu210, wu230)
new_primPlusNat0(Zero, Succ(wu2200), wu230) → new_primPlusNat2(wu2200, wu230)
new_primPlusNat0(Succ(wu210), Succ(wu2200), wu230) → new_primPlusNat2(Succ(new_primPlusNat1(wu210, wu2200)), wu230)
new_primPlusNat0(Zero, Zero, wu230) → new_primPlusNat3(wu230)
new_fromEnum9(wu6) → error([])
new_fromEnum3(wu6) → error([])
new_fromEnum8(wu6) → error([])
new_fromEnum2(@0) → Pos(Zero)
new_fromEnum0(wu6) → error([])
new_fromEnum1(wu6) → error([])
new_fromEnum(wu6, bd) → error([])
new_fromEnum4(wu6) → error([])
new_fromEnum7(wu6) → error([])
new_fromEnum5(wu15, ty_Bool) → new_fromEnum3(wu15)
new_fromEnum5(wu15, ty_Int) → new_fromEnum8(wu15)
new_fromEnum5(wu15, ty_Float) → new_fromEnum0(wu15)
new_fromEnum5(wu15, ty_Ordering) → new_fromEnum9(wu15)
new_fromEnum5(wu15, ty_Double) → new_fromEnum4(wu15)
new_fromEnum5(wu15, ty_Integer) → new_fromEnum1(wu15)
new_fromEnum5(wu15, ty_@0) → new_fromEnum2(wu15)
new_fromEnum5(wu15, ty_Char) → new_fromEnum7(wu15)
new_fromEnum5(wu15, app(ty_Ratio, bf)) → new_fromEnum(wu15, bf)
new_primPlusInt0(Zero, Neg(Zero), Neg(wu230)) → new_primMinusNat1(wu230)
new_primPlusInt0(Succ(wu210), Neg(Succ(wu2200)), Neg(wu230)) → new_primMinusNat0(Succ(new_primPlusNat1(wu210, wu2200)), wu230)
new_primPlusInt0(Zero, Neg(Succ(wu2200)), Neg(wu230)) → new_primMinusNat0(wu2200, wu230)
new_primPlusInt0(Succ(wu210), Neg(Zero), Neg(wu230)) → new_primMinusNat0(wu210, wu230)
new_primPlusInt0(wu21, Neg(wu220), Pos(wu230)) → Pos(new_primPlusNat0(wu21, wu220, wu230))
new_primPlusInt0(wu21, Pos(wu220), wu23) → new_primPlusInt1(wu21, wu220, wu23)

The set Q consists of the following terms:

new_fromEnum6(x0, ty_Ordering)
new_fromEnum8(x0)
new_primMinusNat2(Succ(x0), x1)
new_fromEnum7(x0)
new_primPlusInt0(Succ(x0), Neg(Succ(x1)), Neg(x2))
new_primPlusInt2(Succ(x0), Pos(Zero), Pos(Zero))
new_fromEnum5(x0, ty_Double)
new_primPlusInt1(Succ(x0), Succ(x1), x2)
new_fromEnum5(x0, ty_Ordering)
new_primPlusNat3(Succ(x0))
new_fromEnum6(x0, ty_@0)
new_ps(x0, x1, x2, x3, x4)
new_fromEnum10(x0, ty_Char)
new_fromEnum9(x0)
new_primPlusInt0(Zero, Neg(Succ(x0)), Neg(x1))
new_primPlusInt0(Zero, Neg(Zero), Neg(x0))
new_fromEnum5(x0, ty_Int)
new_primPlusNat1(Zero, Succ(x0))
new_fromEnum10(x0, ty_@0)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primPlusNat2(x0, Zero)
new_primPlusInt1(Succ(x0), Zero, Neg(x1))
new_fromEnum(x0, x1)
new_fromEnum10(x0, ty_Integer)
new_primPlusInt2(Zero, Pos(Succ(x0)), Pos(Zero))
new_primPlusInt1(Zero, Zero, Neg(x0))
new_primPlusNat1(Succ(x0), Zero)
new_primPlusInt2(x0, Neg(x1), x2)
new_primPlusInt0(x0, Pos(x1), x2)
new_fromEnum3(x0)
new_fromEnum6(x0, app(ty_Ratio, x1))
new_primPlusInt2(Succ(x0), Pos(Zero), Pos(Succ(x1)))
new_fromEnum5(x0, ty_@0)
new_primPlusNat0(Succ(x0), Succ(x1), x2)
new_primPlusInt0(Succ(x0), Neg(Zero), Neg(x1))
new_primMinusNat1(Succ(x0))
new_primPlusNat1(Zero, Zero)
new_primPlusNat0(Zero, Zero, x0)
new_fromEnum4(x0)
new_fromEnum6(x0, ty_Bool)
new_fromEnum6(x0, ty_Float)
new_primPlusInt2(Succ(x0), Pos(Succ(x1)), Pos(Zero))
new_fromEnum10(x0, ty_Double)
new_primPlusInt1(Zero, Succ(x0), Neg(x1))
new_primMinusNat3(Zero, Zero)
new_fromEnum5(x0, ty_Integer)
new_fromEnum6(x0, ty_Integer)
new_primPlusInt2(Zero, Pos(Zero), Pos(Succ(x0)))
new_fromEnum1(x0)
new_primPlusInt1(Zero, Zero, Pos(x0))
new_fromEnum10(x0, ty_Int)
new_fromEnum5(x0, ty_Char)
new_primPlusInt2(Succ(x0), Pos(Succ(x1)), Pos(Succ(x2)))
new_fromEnum6(x0, ty_Double)
new_primMinusNat3(Zero, Succ(x0))
new_primMinusNat1(Zero)
new_primPlusInt0(x0, Neg(x1), Pos(x2))
new_primMinusNat3(Succ(x0), Succ(x1))
new_fromEnum5(x0, app(ty_Ratio, x1))
new_fromEnum2(@0)
new_primPlusInt2(x0, Pos(x1), Neg(x2))
new_fromEnum10(x0, ty_Float)
new_fromEnum0(x0)
new_primMinusNat0(x0, Zero)
new_primPlusNat3(Zero)
new_primMinusNat2(Zero, x0)
new_primPlusNat0(Zero, Succ(x0), x1)
new_fromEnum5(x0, ty_Float)
new_fromEnum10(x0, ty_Ordering)
new_primPlusInt1(Succ(x0), Zero, Pos(x1))
new_primPlusInt1(Zero, Succ(x0), Pos(x1))
new_primMinusNat3(Succ(x0), Zero)
new_primPlusNat2(x0, Succ(x1))
new_primPlusInt2(Zero, Pos(Zero), Pos(Zero))
new_fromEnum10(x0, app(ty_Ratio, x1))
new_primPlusInt3(Pos(x0), x1, x2, x3)
new_fromEnum6(x0, ty_Char)
new_primPlusInt2(Zero, Pos(Succ(x0)), Pos(Succ(x1)))
new_primPlusNat0(Succ(x0), Zero, x1)
new_primMinusNat0(x0, Succ(x1))
new_primPlusInt3(Neg(x0), x1, x2, x3)
new_fromEnum6(x0, ty_Int)
new_fromEnum5(x0, ty_Bool)
new_fromEnum10(x0, ty_Bool)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_ps(x0, x1, x2, x3, x4)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ Rewriting

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ MNOCProof

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_map(wu6, wu7, wu8, ba, bb, bc) → new_map(wu6, wu7, new_primPlusInt3(new_fromEnum10(wu6, bb), wu7, wu8, bc), ba, bb, bc)

The TRS R consists of the following rules:

new_fromEnum10(wu6, ty_Float) → new_fromEnum0(wu6)
new_fromEnum10(wu6, ty_Int) → new_fromEnum8(wu6)
new_fromEnum10(wu6, ty_Double) → new_fromEnum4(wu6)
new_fromEnum10(wu6, ty_Integer) → new_fromEnum1(wu6)
new_fromEnum10(wu6, ty_@0) → new_fromEnum2(wu6)
new_fromEnum10(wu6, ty_Bool) → new_fromEnum3(wu6)
new_fromEnum10(wu6, ty_Ordering) → new_fromEnum9(wu6)
new_fromEnum10(wu6, app(ty_Ratio, bd)) → new_fromEnum(wu6, bd)
new_fromEnum10(wu6, ty_Char) → new_fromEnum7(wu6)
new_primPlusInt3(Pos(wu140), wu15, wu16, be) → new_primPlusInt0(wu140, new_fromEnum5(wu15, be), wu16)
new_primPlusInt3(Neg(wu140), wu15, wu16, be) → new_primPlusInt2(wu140, new_fromEnum6(wu15, be), wu16)
new_fromEnum6(wu15, ty_Char) → new_fromEnum7(wu15)
new_fromEnum6(wu15, ty_Double) → new_fromEnum4(wu15)
new_fromEnum6(wu15, app(ty_Ratio, bf)) → new_fromEnum(wu15, bf)
new_fromEnum6(wu15, ty_Integer) → new_fromEnum1(wu15)
new_fromEnum6(wu15, ty_Float) → new_fromEnum0(wu15)
new_fromEnum6(wu15, ty_@0) → new_fromEnum2(wu15)
new_fromEnum6(wu15, ty_Int) → new_fromEnum8(wu15)
new_fromEnum6(wu15, ty_Bool) → new_fromEnum3(wu15)
new_fromEnum6(wu15, ty_Ordering) → new_fromEnum9(wu15)
new_primPlusInt2(Succ(wu280), Pos(Zero), Pos(Zero)) → new_primMinusNat2(Zero, wu280)
new_primPlusInt2(Succ(wu280), Pos(Zero), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), wu280)
new_primPlusInt2(Zero, Pos(Succ(wu2900)), Pos(Zero)) → new_primMinusNat2(Zero, wu2900)
new_primPlusInt2(Zero, Pos(Zero), Pos(Succ(wu3000))) → new_primMinusNat0(wu3000, Zero)
new_primPlusInt2(wu28, Pos(wu290), Neg(wu300)) → Neg(new_primPlusNat0(wu28, wu290, wu300))
new_primPlusInt2(Succ(wu280), Pos(Succ(wu2900)), Pos(Zero)) → new_primMinusNat2(Zero, Succ(new_primPlusNat1(wu280, wu2900)))
new_primPlusInt2(Zero, Pos(Succ(wu2900)), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), wu2900)
new_primPlusInt2(wu28, Neg(wu290), wu30) → new_primPlusInt1(wu290, wu28, wu30)
new_primPlusInt2(Zero, Pos(Zero), Pos(Zero)) → new_primMinusNat1(Zero)
new_primPlusInt2(Succ(wu280), Pos(Succ(wu2900)), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), Succ(new_primPlusNat1(wu280, wu2900)))
new_primPlusNat1(Succ(wu2100), Succ(wu22000)) → Succ(Succ(new_primPlusNat1(wu2100, wu22000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Succ(wu2100), Zero) → Succ(wu2100)
new_primPlusNat1(Zero, Succ(wu22000)) → Succ(wu22000)
new_primMinusNat2(Succ(wu2300), wu2200) → new_primMinusNat3(wu2300, wu2200)
new_primMinusNat3(Zero, Succ(wu23000)) → Neg(Succ(wu23000))
new_primMinusNat3(Succ(wu2100), Zero) → Pos(Succ(wu2100))
new_primMinusNat3(Zero, Zero) → Pos(Zero)
new_primMinusNat3(Succ(wu2100), Succ(wu23000)) → new_primMinusNat3(wu2100, wu23000)
new_primMinusNat1(Zero) → Pos(Zero)
new_primPlusInt1(Succ(wu210), Zero, Pos(wu230)) → Pos(new_primPlusNat2(wu210, wu230))
new_primPlusInt1(Zero, Zero, Pos(wu230)) → Pos(new_primPlusNat3(wu230))
new_primPlusInt1(Zero, Zero, Neg(wu230)) → new_primMinusNat1(wu230)
new_primPlusInt1(Succ(wu210), Zero, Neg(wu230)) → new_primMinusNat0(wu210, wu230)
new_primPlusInt1(Zero, Succ(wu2200), Pos(wu230)) → new_primMinusNat2(wu230, wu2200)
new_primPlusInt1(Zero, Succ(wu2200), Neg(wu230)) → Neg(new_primPlusNat2(wu2200, wu230))
new_primPlusInt1(Succ(wu210), Succ(wu2200), wu23) → new_primPlusInt1(wu210, wu2200, wu23)
new_primPlusNat2(wu210, Succ(wu2300)) → Succ(Succ(new_primPlusNat1(wu210, wu2300)))
new_primPlusNat2(wu210, Zero) → Succ(wu210)
new_primMinusNat2(Zero, wu2200) → Neg(Succ(wu2200))
new_primMinusNat0(wu210, Zero) → Pos(Succ(wu210))
new_primMinusNat0(wu210, Succ(wu2300)) → new_primMinusNat3(wu210, wu2300)
new_primMinusNat1(Succ(wu2300)) → Neg(Succ(wu2300))
new_primPlusNat3(Zero) → Zero
new_primPlusNat3(Succ(wu2300)) → Succ(wu2300)
new_primPlusNat0(Succ(wu210), Zero, wu230) → new_primPlusNat2(wu210, wu230)
new_primPlusNat0(Zero, Succ(wu2200), wu230) → new_primPlusNat2(wu2200, wu230)
new_primPlusNat0(Succ(wu210), Succ(wu2200), wu230) → new_primPlusNat2(Succ(new_primPlusNat1(wu210, wu2200)), wu230)
new_primPlusNat0(Zero, Zero, wu230) → new_primPlusNat3(wu230)
new_fromEnum9(wu6) → error([])
new_fromEnum3(wu6) → error([])
new_fromEnum8(wu6) → error([])
new_fromEnum2(@0) → Pos(Zero)
new_fromEnum0(wu6) → error([])
new_fromEnum1(wu6) → error([])
new_fromEnum(wu6, bd) → error([])
new_fromEnum4(wu6) → error([])
new_fromEnum7(wu6) → error([])
new_fromEnum5(wu15, ty_Bool) → new_fromEnum3(wu15)
new_fromEnum5(wu15, ty_Int) → new_fromEnum8(wu15)
new_fromEnum5(wu15, ty_Float) → new_fromEnum0(wu15)
new_fromEnum5(wu15, ty_Ordering) → new_fromEnum9(wu15)
new_fromEnum5(wu15, ty_Double) → new_fromEnum4(wu15)
new_fromEnum5(wu15, ty_Integer) → new_fromEnum1(wu15)
new_fromEnum5(wu15, ty_@0) → new_fromEnum2(wu15)
new_fromEnum5(wu15, ty_Char) → new_fromEnum7(wu15)
new_fromEnum5(wu15, app(ty_Ratio, bf)) → new_fromEnum(wu15, bf)
new_primPlusInt0(Zero, Neg(Zero), Neg(wu230)) → new_primMinusNat1(wu230)
new_primPlusInt0(Succ(wu210), Neg(Succ(wu2200)), Neg(wu230)) → new_primMinusNat0(Succ(new_primPlusNat1(wu210, wu2200)), wu230)
new_primPlusInt0(Zero, Neg(Succ(wu2200)), Neg(wu230)) → new_primMinusNat0(wu2200, wu230)
new_primPlusInt0(Succ(wu210), Neg(Zero), Neg(wu230)) → new_primMinusNat0(wu210, wu230)
new_primPlusInt0(wu21, Neg(wu220), Pos(wu230)) → Pos(new_primPlusNat0(wu21, wu220, wu230))
new_primPlusInt0(wu21, Pos(wu220), wu23) → new_primPlusInt1(wu21, wu220, wu23)

The set Q consists of the following terms:

new_fromEnum6(x0, ty_Ordering)
new_fromEnum8(x0)
new_primMinusNat2(Succ(x0), x1)
new_fromEnum7(x0)
new_primPlusInt0(Succ(x0), Neg(Succ(x1)), Neg(x2))
new_primPlusInt2(Succ(x0), Pos(Zero), Pos(Zero))
new_fromEnum5(x0, ty_Double)
new_primPlusInt1(Succ(x0), Succ(x1), x2)
new_fromEnum5(x0, ty_Ordering)
new_primPlusNat3(Succ(x0))
new_fromEnum6(x0, ty_@0)
new_fromEnum10(x0, ty_Char)
new_fromEnum9(x0)
new_primPlusInt0(Zero, Neg(Succ(x0)), Neg(x1))
new_primPlusInt0(Zero, Neg(Zero), Neg(x0))
new_fromEnum5(x0, ty_Int)
new_primPlusNat1(Zero, Succ(x0))
new_fromEnum10(x0, ty_@0)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primPlusNat2(x0, Zero)
new_primPlusInt1(Succ(x0), Zero, Neg(x1))
new_fromEnum(x0, x1)
new_fromEnum10(x0, ty_Integer)
new_primPlusInt2(Zero, Pos(Succ(x0)), Pos(Zero))
new_primPlusInt1(Zero, Zero, Neg(x0))
new_primPlusNat1(Succ(x0), Zero)
new_primPlusInt2(x0, Neg(x1), x2)
new_primPlusInt0(x0, Pos(x1), x2)
new_fromEnum3(x0)
new_fromEnum6(x0, app(ty_Ratio, x1))
new_primPlusInt2(Succ(x0), Pos(Zero), Pos(Succ(x1)))
new_fromEnum5(x0, ty_@0)
new_primPlusNat0(Succ(x0), Succ(x1), x2)
new_primPlusInt0(Succ(x0), Neg(Zero), Neg(x1))
new_primMinusNat1(Succ(x0))
new_primPlusNat1(Zero, Zero)
new_primPlusNat0(Zero, Zero, x0)
new_fromEnum4(x0)
new_fromEnum6(x0, ty_Bool)
new_fromEnum6(x0, ty_Float)
new_primPlusInt2(Succ(x0), Pos(Succ(x1)), Pos(Zero))
new_fromEnum10(x0, ty_Double)
new_primPlusInt1(Zero, Succ(x0), Neg(x1))
new_primMinusNat3(Zero, Zero)
new_fromEnum5(x0, ty_Integer)
new_fromEnum6(x0, ty_Integer)
new_primPlusInt2(Zero, Pos(Zero), Pos(Succ(x0)))
new_fromEnum1(x0)
new_primPlusInt1(Zero, Zero, Pos(x0))
new_fromEnum10(x0, ty_Int)
new_fromEnum5(x0, ty_Char)
new_primPlusInt2(Succ(x0), Pos(Succ(x1)), Pos(Succ(x2)))
new_fromEnum6(x0, ty_Double)
new_primMinusNat3(Zero, Succ(x0))
new_primMinusNat1(Zero)
new_primPlusInt0(x0, Neg(x1), Pos(x2))
new_primMinusNat3(Succ(x0), Succ(x1))
new_fromEnum5(x0, app(ty_Ratio, x1))
new_fromEnum2(@0)
new_primPlusInt2(x0, Pos(x1), Neg(x2))
new_fromEnum10(x0, ty_Float)
new_fromEnum0(x0)
new_primMinusNat0(x0, Zero)
new_primPlusNat3(Zero)
new_primMinusNat2(Zero, x0)
new_primPlusNat0(Zero, Succ(x0), x1)
new_fromEnum5(x0, ty_Float)
new_fromEnum10(x0, ty_Ordering)
new_primPlusInt1(Succ(x0), Zero, Pos(x1))
new_primPlusInt1(Zero, Succ(x0), Pos(x1))
new_primMinusNat3(Succ(x0), Zero)
new_primPlusNat2(x0, Succ(x1))
new_primPlusInt2(Zero, Pos(Zero), Pos(Zero))
new_fromEnum10(x0, app(ty_Ratio, x1))
new_primPlusInt3(Pos(x0), x1, x2, x3)
new_fromEnum6(x0, ty_Char)
new_primPlusInt2(Zero, Pos(Succ(x0)), Pos(Succ(x1)))
new_primPlusNat0(Succ(x0), Zero, x1)
new_primMinusNat0(x0, Succ(x1))
new_primPlusInt3(Neg(x0), x1, x2, x3)
new_fromEnum6(x0, ty_Int)
new_fromEnum5(x0, ty_Bool)
new_fromEnum10(x0, ty_Bool)

We have to consider all minimal (P,Q,R)-chains.
We use the modular non-overlap check [17] to decrease Q to the empty set.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ Rewriting

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ MNOCProof

                                  ↳ QDP

                                    ↳ NonTerminationProof

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_map(wu6, wu7, wu8, ba, bb, bc) → new_map(wu6, wu7, new_primPlusInt3(new_fromEnum10(wu6, bb), wu7, wu8, bc), ba, bb, bc)

The TRS R consists of the following rules:

new_fromEnum10(wu6, ty_Float) → new_fromEnum0(wu6)
new_fromEnum10(wu6, ty_Int) → new_fromEnum8(wu6)
new_fromEnum10(wu6, ty_Double) → new_fromEnum4(wu6)
new_fromEnum10(wu6, ty_Integer) → new_fromEnum1(wu6)
new_fromEnum10(wu6, ty_@0) → new_fromEnum2(wu6)
new_fromEnum10(wu6, ty_Bool) → new_fromEnum3(wu6)
new_fromEnum10(wu6, ty_Ordering) → new_fromEnum9(wu6)
new_fromEnum10(wu6, app(ty_Ratio, bd)) → new_fromEnum(wu6, bd)
new_fromEnum10(wu6, ty_Char) → new_fromEnum7(wu6)
new_primPlusInt3(Pos(wu140), wu15, wu16, be) → new_primPlusInt0(wu140, new_fromEnum5(wu15, be), wu16)
new_primPlusInt3(Neg(wu140), wu15, wu16, be) → new_primPlusInt2(wu140, new_fromEnum6(wu15, be), wu16)
new_fromEnum6(wu15, ty_Char) → new_fromEnum7(wu15)
new_fromEnum6(wu15, ty_Double) → new_fromEnum4(wu15)
new_fromEnum6(wu15, app(ty_Ratio, bf)) → new_fromEnum(wu15, bf)
new_fromEnum6(wu15, ty_Integer) → new_fromEnum1(wu15)
new_fromEnum6(wu15, ty_Float) → new_fromEnum0(wu15)
new_fromEnum6(wu15, ty_@0) → new_fromEnum2(wu15)
new_fromEnum6(wu15, ty_Int) → new_fromEnum8(wu15)
new_fromEnum6(wu15, ty_Bool) → new_fromEnum3(wu15)
new_fromEnum6(wu15, ty_Ordering) → new_fromEnum9(wu15)
new_primPlusInt2(Succ(wu280), Pos(Zero), Pos(Zero)) → new_primMinusNat2(Zero, wu280)
new_primPlusInt2(Succ(wu280), Pos(Zero), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), wu280)
new_primPlusInt2(Zero, Pos(Succ(wu2900)), Pos(Zero)) → new_primMinusNat2(Zero, wu2900)
new_primPlusInt2(Zero, Pos(Zero), Pos(Succ(wu3000))) → new_primMinusNat0(wu3000, Zero)
new_primPlusInt2(wu28, Pos(wu290), Neg(wu300)) → Neg(new_primPlusNat0(wu28, wu290, wu300))
new_primPlusInt2(Succ(wu280), Pos(Succ(wu2900)), Pos(Zero)) → new_primMinusNat2(Zero, Succ(new_primPlusNat1(wu280, wu2900)))
new_primPlusInt2(Zero, Pos(Succ(wu2900)), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), wu2900)
new_primPlusInt2(wu28, Neg(wu290), wu30) → new_primPlusInt1(wu290, wu28, wu30)
new_primPlusInt2(Zero, Pos(Zero), Pos(Zero)) → new_primMinusNat1(Zero)
new_primPlusInt2(Succ(wu280), Pos(Succ(wu2900)), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), Succ(new_primPlusNat1(wu280, wu2900)))
new_primPlusNat1(Succ(wu2100), Succ(wu22000)) → Succ(Succ(new_primPlusNat1(wu2100, wu22000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Succ(wu2100), Zero) → Succ(wu2100)
new_primPlusNat1(Zero, Succ(wu22000)) → Succ(wu22000)
new_primMinusNat2(Succ(wu2300), wu2200) → new_primMinusNat3(wu2300, wu2200)
new_primMinusNat3(Zero, Succ(wu23000)) → Neg(Succ(wu23000))
new_primMinusNat3(Succ(wu2100), Zero) → Pos(Succ(wu2100))
new_primMinusNat3(Zero, Zero) → Pos(Zero)
new_primMinusNat3(Succ(wu2100), Succ(wu23000)) → new_primMinusNat3(wu2100, wu23000)
new_primMinusNat1(Zero) → Pos(Zero)
new_primPlusInt1(Succ(wu210), Zero, Pos(wu230)) → Pos(new_primPlusNat2(wu210, wu230))
new_primPlusInt1(Zero, Zero, Pos(wu230)) → Pos(new_primPlusNat3(wu230))
new_primPlusInt1(Zero, Zero, Neg(wu230)) → new_primMinusNat1(wu230)
new_primPlusInt1(Succ(wu210), Zero, Neg(wu230)) → new_primMinusNat0(wu210, wu230)
new_primPlusInt1(Zero, Succ(wu2200), Pos(wu230)) → new_primMinusNat2(wu230, wu2200)
new_primPlusInt1(Zero, Succ(wu2200), Neg(wu230)) → Neg(new_primPlusNat2(wu2200, wu230))
new_primPlusInt1(Succ(wu210), Succ(wu2200), wu23) → new_primPlusInt1(wu210, wu2200, wu23)
new_primPlusNat2(wu210, Succ(wu2300)) → Succ(Succ(new_primPlusNat1(wu210, wu2300)))
new_primPlusNat2(wu210, Zero) → Succ(wu210)
new_primMinusNat2(Zero, wu2200) → Neg(Succ(wu2200))
new_primMinusNat0(wu210, Zero) → Pos(Succ(wu210))
new_primMinusNat0(wu210, Succ(wu2300)) → new_primMinusNat3(wu210, wu2300)
new_primMinusNat1(Succ(wu2300)) → Neg(Succ(wu2300))
new_primPlusNat3(Zero) → Zero
new_primPlusNat3(Succ(wu2300)) → Succ(wu2300)
new_primPlusNat0(Succ(wu210), Zero, wu230) → new_primPlusNat2(wu210, wu230)
new_primPlusNat0(Zero, Succ(wu2200), wu230) → new_primPlusNat2(wu2200, wu230)
new_primPlusNat0(Succ(wu210), Succ(wu2200), wu230) → new_primPlusNat2(Succ(new_primPlusNat1(wu210, wu2200)), wu230)
new_primPlusNat0(Zero, Zero, wu230) → new_primPlusNat3(wu230)
new_fromEnum9(wu6) → error([])
new_fromEnum3(wu6) → error([])
new_fromEnum8(wu6) → error([])
new_fromEnum2(@0) → Pos(Zero)
new_fromEnum0(wu6) → error([])
new_fromEnum1(wu6) → error([])
new_fromEnum(wu6, bd) → error([])
new_fromEnum4(wu6) → error([])
new_fromEnum7(wu6) → error([])
new_fromEnum5(wu15, ty_Bool) → new_fromEnum3(wu15)
new_fromEnum5(wu15, ty_Int) → new_fromEnum8(wu15)
new_fromEnum5(wu15, ty_Float) → new_fromEnum0(wu15)
new_fromEnum5(wu15, ty_Ordering) → new_fromEnum9(wu15)
new_fromEnum5(wu15, ty_Double) → new_fromEnum4(wu15)
new_fromEnum5(wu15, ty_Integer) → new_fromEnum1(wu15)
new_fromEnum5(wu15, ty_@0) → new_fromEnum2(wu15)
new_fromEnum5(wu15, ty_Char) → new_fromEnum7(wu15)
new_fromEnum5(wu15, app(ty_Ratio, bf)) → new_fromEnum(wu15, bf)
new_primPlusInt0(Zero, Neg(Zero), Neg(wu230)) → new_primMinusNat1(wu230)
new_primPlusInt0(Succ(wu210), Neg(Succ(wu2200)), Neg(wu230)) → new_primMinusNat0(Succ(new_primPlusNat1(wu210, wu2200)), wu230)
new_primPlusInt0(Zero, Neg(Succ(wu2200)), Neg(wu230)) → new_primMinusNat0(wu2200, wu230)
new_primPlusInt0(Succ(wu210), Neg(Zero), Neg(wu230)) → new_primMinusNat0(wu210, wu230)
new_primPlusInt0(wu21, Neg(wu220), Pos(wu230)) → Pos(new_primPlusNat0(wu21, wu220, wu230))
new_primPlusInt0(wu21, Pos(wu220), wu23) → new_primPlusInt1(wu21, wu220, wu23)

Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_map(wu6, wu7, wu8, ba, bb, bc) → new_map(wu6, wu7, new_primPlusInt3(new_fromEnum10(wu6, bb), wu7, wu8, bc), ba, bb, bc)

The TRS R consists of the following rules:

new_fromEnum10(wu6, ty_Float) → new_fromEnum0(wu6)
new_fromEnum10(wu6, ty_Int) → new_fromEnum8(wu6)
new_fromEnum10(wu6, ty_Double) → new_fromEnum4(wu6)
new_fromEnum10(wu6, ty_Integer) → new_fromEnum1(wu6)
new_fromEnum10(wu6, ty_@0) → new_fromEnum2(wu6)
new_fromEnum10(wu6, ty_Bool) → new_fromEnum3(wu6)
new_fromEnum10(wu6, ty_Ordering) → new_fromEnum9(wu6)
new_fromEnum10(wu6, app(ty_Ratio, bd)) → new_fromEnum(wu6, bd)
new_fromEnum10(wu6, ty_Char) → new_fromEnum7(wu6)
new_primPlusInt3(Pos(wu140), wu15, wu16, be) → new_primPlusInt0(wu140, new_fromEnum5(wu15, be), wu16)
new_primPlusInt3(Neg(wu140), wu15, wu16, be) → new_primPlusInt2(wu140, new_fromEnum6(wu15, be), wu16)
new_fromEnum6(wu15, ty_Char) → new_fromEnum7(wu15)
new_fromEnum6(wu15, ty_Double) → new_fromEnum4(wu15)
new_fromEnum6(wu15, app(ty_Ratio, bf)) → new_fromEnum(wu15, bf)
new_fromEnum6(wu15, ty_Integer) → new_fromEnum1(wu15)
new_fromEnum6(wu15, ty_Float) → new_fromEnum0(wu15)
new_fromEnum6(wu15, ty_@0) → new_fromEnum2(wu15)
new_fromEnum6(wu15, ty_Int) → new_fromEnum8(wu15)
new_fromEnum6(wu15, ty_Bool) → new_fromEnum3(wu15)
new_fromEnum6(wu15, ty_Ordering) → new_fromEnum9(wu15)
new_primPlusInt2(Succ(wu280), Pos(Zero), Pos(Zero)) → new_primMinusNat2(Zero, wu280)
new_primPlusInt2(Succ(wu280), Pos(Zero), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), wu280)
new_primPlusInt2(Zero, Pos(Succ(wu2900)), Pos(Zero)) → new_primMinusNat2(Zero, wu2900)
new_primPlusInt2(Zero, Pos(Zero), Pos(Succ(wu3000))) → new_primMinusNat0(wu3000, Zero)
new_primPlusInt2(wu28, Pos(wu290), Neg(wu300)) → Neg(new_primPlusNat0(wu28, wu290, wu300))
new_primPlusInt2(Succ(wu280), Pos(Succ(wu2900)), Pos(Zero)) → new_primMinusNat2(Zero, Succ(new_primPlusNat1(wu280, wu2900)))
new_primPlusInt2(Zero, Pos(Succ(wu2900)), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), wu2900)
new_primPlusInt2(wu28, Neg(wu290), wu30) → new_primPlusInt1(wu290, wu28, wu30)
new_primPlusInt2(Zero, Pos(Zero), Pos(Zero)) → new_primMinusNat1(Zero)
new_primPlusInt2(Succ(wu280), Pos(Succ(wu2900)), Pos(Succ(wu3000))) → new_primMinusNat2(Succ(wu3000), Succ(new_primPlusNat1(wu280, wu2900)))
new_primPlusNat1(Succ(wu2100), Succ(wu22000)) → Succ(Succ(new_primPlusNat1(wu2100, wu22000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Succ(wu2100), Zero) → Succ(wu2100)
new_primPlusNat1(Zero, Succ(wu22000)) → Succ(wu22000)
new_primMinusNat2(Succ(wu2300), wu2200) → new_primMinusNat3(wu2300, wu2200)
new_primMinusNat3(Zero, Succ(wu23000)) → Neg(Succ(wu23000))
new_primMinusNat3(Succ(wu2100), Zero) → Pos(Succ(wu2100))
new_primMinusNat3(Zero, Zero) → Pos(Zero)
new_primMinusNat3(Succ(wu2100), Succ(wu23000)) → new_primMinusNat3(wu2100, wu23000)
new_primMinusNat1(Zero) → Pos(Zero)
new_primPlusInt1(Succ(wu210), Zero, Pos(wu230)) → Pos(new_primPlusNat2(wu210, wu230))
new_primPlusInt1(Zero, Zero, Pos(wu230)) → Pos(new_primPlusNat3(wu230))
new_primPlusInt1(Zero, Zero, Neg(wu230)) → new_primMinusNat1(wu230)
new_primPlusInt1(Succ(wu210), Zero, Neg(wu230)) → new_primMinusNat0(wu210, wu230)
new_primPlusInt1(Zero, Succ(wu2200), Pos(wu230)) → new_primMinusNat2(wu230, wu2200)
new_primPlusInt1(Zero, Succ(wu2200), Neg(wu230)) → Neg(new_primPlusNat2(wu2200, wu230))
new_primPlusInt1(Succ(wu210), Succ(wu2200), wu23) → new_primPlusInt1(wu210, wu2200, wu23)
new_primPlusNat2(wu210, Succ(wu2300)) → Succ(Succ(new_primPlusNat1(wu210, wu2300)))
new_primPlusNat2(wu210, Zero) → Succ(wu210)
new_primMinusNat2(Zero, wu2200) → Neg(Succ(wu2200))
new_primMinusNat0(wu210, Zero) → Pos(Succ(wu210))
new_primMinusNat0(wu210, Succ(wu2300)) → new_primMinusNat3(wu210, wu2300)
new_primMinusNat1(Succ(wu2300)) → Neg(Succ(wu2300))
new_primPlusNat3(Zero) → Zero
new_primPlusNat3(Succ(wu2300)) → Succ(wu2300)
new_primPlusNat0(Succ(wu210), Zero, wu230) → new_primPlusNat2(wu210, wu230)
new_primPlusNat0(Zero, Succ(wu2200), wu230) → new_primPlusNat2(wu2200, wu230)
new_primPlusNat0(Succ(wu210), Succ(wu2200), wu230) → new_primPlusNat2(Succ(new_primPlusNat1(wu210, wu2200)), wu230)
new_primPlusNat0(Zero, Zero, wu230) → new_primPlusNat3(wu230)
new_fromEnum9(wu6) → error([])
new_fromEnum3(wu6) → error([])
new_fromEnum8(wu6) → error([])
new_fromEnum2(@0) → Pos(Zero)
new_fromEnum0(wu6) → error([])
new_fromEnum1(wu6) → error([])
new_fromEnum(wu6, bd) → error([])
new_fromEnum4(wu6) → error([])
new_fromEnum7(wu6) → error([])
new_fromEnum5(wu15, ty_Bool) → new_fromEnum3(wu15)
new_fromEnum5(wu15, ty_Int) → new_fromEnum8(wu15)
new_fromEnum5(wu15, ty_Float) → new_fromEnum0(wu15)
new_fromEnum5(wu15, ty_Ordering) → new_fromEnum9(wu15)
new_fromEnum5(wu15, ty_Double) → new_fromEnum4(wu15)
new_fromEnum5(wu15, ty_Integer) → new_fromEnum1(wu15)
new_fromEnum5(wu15, ty_@0) → new_fromEnum2(wu15)
new_fromEnum5(wu15, ty_Char) → new_fromEnum7(wu15)
new_fromEnum5(wu15, app(ty_Ratio, bf)) → new_fromEnum(wu15, bf)
new_primPlusInt0(Zero, Neg(Zero), Neg(wu230)) → new_primMinusNat1(wu230)
new_primPlusInt0(Succ(wu210), Neg(Succ(wu2200)), Neg(wu230)) → new_primMinusNat0(Succ(new_primPlusNat1(wu210, wu2200)), wu230)
new_primPlusInt0(Zero, Neg(Succ(wu2200)), Neg(wu230)) → new_primMinusNat0(wu2200, wu230)
new_primPlusInt0(Succ(wu210), Neg(Zero), Neg(wu230)) → new_primMinusNat0(wu210, wu230)
new_primPlusInt0(wu21, Neg(wu220), Pos(wu230)) → Pos(new_primPlusNat0(wu21, wu220, wu230))
new_primPlusInt0(wu21, Pos(wu220), wu23) → new_primPlusInt1(wu21, wu220, wu23)

s = new_map(wu6, wu7, wu8, ba, bb, bc) evaluates to t =new_map(wu6, wu7, new_primPlusInt3(new_fromEnum10(wu6, bb), wu7, wu8, bc), ba, bb, bc)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [wu8 / new_primPlusInt3(new_fromEnum10(wu6, bb), wu7, wu8, bc)]
Semiunifier: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_map(wu6, wu7, wu8, ba, bb, bc) to new_map(wu6, wu7, new_primPlusInt3(new_fromEnum10(wu6, bb), wu7, wu8, bc), ba, bb, bc).

Haskell To QDPs